Loading...
Please wait, while we are loading the content...
Similar Documents
Synthesis of Concurrent Systems for an Atomic Read / Atomic Write Model of Computation (Extended Abstract) (1996)
| Content Provider | CiteSeerX |
|---|---|
| Author | Attie, Paul C. Emerson, E. Allen |
| Description | Proc. 15'th ACM PODC Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed (cf. [EC82, MW84, PR89, PR89b, AM94]). An important advantage of these synthesis methods is that they obviate the need to manually construct a program and compose a proof of its correctness. A serious drawback of these methods in practice, however, is that they produce concurrent programs for models of computation that are often unrealistic, involving highly centralized system architecture (cf. [MW84]) or processes with global information about the system state (cf. [EC82]). Even simple synchronization protocols based on atomic read / atomic write primitives such as Peterson's solution to the mutual exclusion problem have remained outside the scope of practical mechanical synthesis methods. In this paper, we show how to mechanically synthesize in more realistic computational models solutions to synchronization problems. We illustrate the method by synthesizing Peterson's solution to the mutual exclusion problem. |
| File Format | |
| Language | English |
| Publisher Date | 1996-01-01 |
| Access Restriction | Open |
| Subject Keyword | Atomic Read Atomic Write Model Extended Abstract Serious Drawback Important Advantage Global Information Mutual Exclusion Problem Temporal Logic Specification Concurrent System System State System Architecture Atomic Read Atomic Write Primitive Synthesis Method Simple Synchronization Protocol Practical Mechanical Synthesis Method Concurrent Program Realistic Computational Model Solution |
| Content Type | Text |
| Resource Type | Article |
