A Caltech Library Service

Distributed Diners: From UNITY Specification to CC++ Implementation

Binau, Ulla (1993) Distributed Diners: From UNITY Specification to CC++ Implementation. Computer Science Technical Reports, California Institute of Technology , Pasadena, CA. (Unpublished)

Postscript - Submitted Version
See Usage Policy.

[img] PDF - Submitted Version
See Usage Policy.


Use this Persistent URL to link to this item:


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].

Item Type:Report or Paper (Technical Report)
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.
Group:Computer Science Technical Reports
Series Name:Computer Science Technical Reports
Record Number:CaltechCSTR:1993.cs-tr-93-20
Persistent URL:
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:26867
Deposited By: Imported from CaltechCSTR
Deposited On:14 May 2001
Last Modified:03 Oct 2019 03:18

Repository Staff Only: item control page