Conference item icon

Conference item

Verification of tree-based hierarchical read-copy update in the Linux kernel

Abstract:

Read-Copy Update (RCU) is a scalable, high-performance Linux-kernel synchronization mechanism that runs low-overhead readers concurrently with updaters. Production-quality RCU implementations are decidedly non-trivial and their stringent validation is mandatory. This suggests use of formal verification. Previous formal verification efforts for RCU either focus on simple implementations or use modeling languages. In this paper, we construct a model directly from the source code of Tree RCU in ...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.23919/DATE.2018.8341980

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS Division
Department:
Computer Science
Oxford college:
Balliol College
Role:
Author
Publisher:
IEEE Publisher's website
Pages:
61-66
Publication date:
2018-04-23
Acceptance date:
2017-11-10
DOI:
ISSN:
1558-1101
Pubs id:
pubs:745086
URN:
uri:b8ec1f29-39f7-4280-834c-4a022bb46ba1
UUID:
uuid:b8ec1f29-39f7-4280-834c-4a022bb46ba1
Local pid:
pubs:745086
ISBN:
978-3-9819263-0-9

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP