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 May 14, 2001 | Submitted
Report Open

Distributed Diners: From UNITY Specification to CC++ Implementation

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

93-20.pdf
Files (563.0 kB)
Name Size Download all
md5:9f2282c283c1b488e0ecf0024a33f07f
276.1 kB Preview Download
md5:beada761adb960c2cccb9351110f79fb
286.9 kB Download

Additional details

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