Published January 1, 1992
| Version Submitted
Technical Report
Open
Mutual Exclusion in a Token Ring in CC++
Creators
Abstract
This report describes a first attempt at using UNITY to verify reactive Compositional C++ (CC++) programs. We propose a distributed solution to the mutual exclusion problem using partially synchronous communication channels. The solution is described as a CC++ program, from which a small set of "basic" properties is derived. Using UNITY, we proof mutual exclusion and progress of the solution based on the set of properties derived from the code.
Additional Information
© 1992 California Institute of Technology. A warm thanks to my colleagues at Caltech for many useful discussions. In particular to my fellow students, Peter Hofstee, Marcel van der Goot, and Rustan Leino, and to Ralph Back and Jan van de Snepscheut who all found time to read and discuss an earliear version of this report, supplied many useful comments, and pointed out a number of interesting references. Also thanks to Marcel van der Goot for producing an environment for presenting the CC++ programs overnight. Last (but definitely not least) to Mani Chandy who advised me in my work and without whom this would never have come through.Attached Files
Submitted - postscript.pdf
Submitted - postscript.ps
Files
postscript.pdf
Files
(466.7 kB)
| Name | Size | Download all |
|---|---|---|
|
md5:e681108a3c31a9b4f542c214e17d4635
|
259.2 kB | Preview Download |
|
md5:496a85d4f29899d0a354681f302f194e
|
207.4 kB | Download |
Additional details
Identifiers
- Eprint ID
- 26755
- Resolver ID
- CaltechCSTR:1992.cs-tr-92-11
Dates
- Created
-
2001-04-25Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
Caltech Custom Metadata
- Caltech groups
- Computer Science Technical Reports
- Series Name
- Computer Science Technical Reports
- Other Numbering System Name
- Copmuter Science Technical Report
- Other Numbering System Identifier
- 92-11