Distributed Diners: From UNITY Specification to CC++ Implementation
- Creators
- Binau, Ulla
Abstract
Resource conflicts may typically be described as the dining philosophers problem (or diners for short). In this report we derive a distributed message-passing solution to the diners problem from the shared memory solution presented in [CM88, Ch.12 Dining Philosophers]. We define an isomorphism between variables in the shared memory state and variables in the distributed state. This allows us to translate the shared memory UNITY specification to a distributed UNITY specification without affecting the validity of the original refinement proof. It turns out that the translated progress properties cannot be fulfilled by the solution scheme we have in mind. However, we show that weaker properties may be used instead, still without affecting the correctness of the original proof. The derivation of a UNITY program from the translated properties is not quite obvious. Hence we introduce an extra refinement step prior to deriving our distributed UNITY implementation. Finally the distributed UNITY implementation is translated to Compositional C++, (CC++) a parallel extension of C and C++. Note: The reader is assumed to be familiar with UNITY [CM88] and C, C++ or CC++ [KR88, Str91, CK92].
Additional Information
© 1993 California Institute of Technology. June 3, 1993. The further refinement of the final of specification in [CM88] as opposed to a refinement from scratch was inspired by Singh's work on program refinement [Sin 92]. Mani Chandy inspired the functional programming idea behind the CC++ program, and I would like to thank him for his very valuable support during my work. Also thanks to Rustan Leino and Peter Hofstee for a good push, when Mani Chandy's group at Caltech for many good discussions and their extensive comments to an earlier version of this report.Attached Files
Submitted - 93-20.pdf
Submitted - 93-20.ps
Files
Additional details
- Eprint ID
- 26867
- Resolver ID
- CaltechCSTR:1993.cs-tr-93-20
- Created
-
2001-05-14Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Computer Science Technical Reports
- Series Name
- Computer Science Technical Reports