Loading...
Please wait, while we are loading the content...
Similar Documents
Modular progress proofs of asynchronous programs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Cohen, Ernest Samuel |
| Copyright Year | 1993 |
| Abstract | The usual way to reason about a concurrent program is to prove that it preserves certain state predicates; such predicates are said to be stable. However, many important techniques of concurrent program construction (e.g., pipelining) depend on commutativity conditions between actions, which cannot be directly expressed using stability; in fact, these techniques lie beyond ordinary state-based program reasoning. In this thesis, we show how to handle these techniques in a natural way by generalizing stability of predicates to stability of predicate transformers. Based on this generalization, we give semantic conditions under which we can pretend that a program inherits progress properties from one of its components, and a rich calculus for constructing these "decoupled" components. Moreover, if a decoupled component restores the system to some predicate, then we can "pretend" that the predicate is stable (in a weak sense), and thus simplify the stats that have to be considered in analysing the program. We use our theory to reprove and extend some of Misra's results on "loosely-coupled" programs, and to construct new program-logical proofs of the window protocol for communication across noisy channels and the tree protocol for serializable transaction processing. |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
