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:
-
-
(Version of record, pdf, 383.5KB)
-
(Version of record, pdf, 372.8KB)
-
- Publisher copy:
- 10.1007/s00165-019-00487-y
Authors
Bibliographic Details
- Publisher:
- Springer Nature Publisher's website
- Journal:
- Formal Aspects of Computing Journal website
- Volume:
- 31
- Issue:
- 4
- Pages:
- 411–419
- Publication date:
- 2019-07-15
- Acceptance date:
- 2019-06-26
- DOI:
- EISSN:
-
1433-299X
- ISSN:
-
0934-5043
Item Description
- 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
- Copyright holder:
- Lowe, G
- Copyright date:
- 2019
- Notes:
- © The Author(s) 2019. Open Access. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License, which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
- Licence:
- CC Attribution (CC BY)
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record