Binau, Ulla (1993) Distributed Diners: From UNITY Specification to CC++ Implementation. California Institute of Technology . (Unpublished) http://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-20
See Usage Policy.
Other (Adobe PDF (332KB))
See Usage Policy.
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1993.cs-tr-93-20
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)|
|Group:||Computer Science Technical Reports|
|Usage Policy:||You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.|
|Deposited By:||Imported from CaltechCSTR|
|Deposited On:||14 May 2001|
|Last Modified:||26 Dec 2012 14:08|
Repository Staff Only: item control page