Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published April 25, 2001 | Submitted
Report Open

Mutual Exclusion in a Token Ring in CC++

Binau, Ulla

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

Created:
August 20, 2023
Modified:
January 13, 2024