Journal article icon

Journal article

Discovering and correcting a deadlock in a channel implementation

Abstract:
We investigate the cause of a deadlock in the implementation of a channel in a message-passing concurrency API. We model the channel implementation using the process algebra CSP, and then use the model checker FDR to find the cause of the deadlock. The bug is rather subtle, and arguably infeasible to spot by hand. We then propose a straightforward fix to the bug, and use CSP and FDR to verify this fix.
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/s00165-019-00487-y

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
St Catherine's College
Role:
Author
Publisher:
Springer Nature
Journal:
Formal Aspects of Computing More from this journal
Volume:
31
Issue:
4
Pages:
411–419
Publication date:
2019-07-15
Acceptance date:
2019-06-26
DOI:
EISSN:
1433-299X
ISSN:
0934-5043
Keywords:
Pubs id:
pubs:1011764
UUID:
uuid:8ae5e225-d449-4ee4-9a42-ff22471e6bfa
Local pid:
pubs:1011764
Source identifiers:
1011764
Deposit date:
2019-06-12

Terms of use


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