A Discipline of Multiprogramming Programming Theory for Distributed Applications

In this book, a programming model is developed that addresses the fundamental issues of "large-scale programming," unifying several concepts from database theory, object-oriented programming and designs of reactive systems. The model and the associated theory have been christened "Seuss." The major goal of Seuss is to simplify multiprogramming. To this end, we separate the concern of concurrent implementation from the core program design problem. A program execution is understood as a single thread of control - sequential executions of actions that are chosen according to some scheduling policy - yet program implementation permits concurrent executions of multiple threads. As a consequence, it is possible to reason about the properties of a program from its single execution thread, whereas an implementation may exploit the inherent concurrency for efficient execution.

A Discipline of Multiprogramming.- 1.1 Wide-Area Computing.- 1.2 An Example: Planning a Meeting.- 1.3 Issues in Multiprogram Design.- 1.4 Concluding Remarks.- 1.5 Bibliographic Notes.- 2 Action Systems.- 2.1 An Informal View of Action Systems.- 2.2 Syntax and Semantics of Action Systems.- 2.3 Properties of Action Systems.- 2.4 Examples.- 2.5 Concluding Remarks.- 2.6 Bibliographic Notes.- 3 An Object-Oriented View of Action Systems.- 3.1 Introduction.- 3.2 Seuss Syntax.- 3.3 Seuss Semantics (Operational).- 3.4 Discussion.- 3.5 Concluding Remarks.- 3.6 Bibliographic Notes.- 4 Small Examples.- 4.1 Channels.- 4.2 A Simple Database.- 4.3 Management of Multilevel Memory: Lazy Caching.- 4.4 Real-Time Controller; Discrete-Event Simulation.- 4.5 Example of a Process Network.- 4.6 Broadcast.- 4.7 Barrier Synchronization.- 4.8 Readers and Writers.- 4.9 Semaphore.- 4.10 Multiple Resource Allocation.- 4.11 Concluding Remarks.- 4.12 Bibliographic Notes.- 5 Safety Properties.- 5.1 Introduction.- 5.2 The Meaning of co.- 5.3 Special Cases of co.- 5.4 Derived Rules.- 5.5 Applications.- 5.6 Theoretical Results.- 5.7 Concluding Remarks.- 5.8 Bibliographic Notes.- 5.9 Exercises.- 5.10 Solutions to Exercises.- 6 Progress Properties.- 6.1 Introduction.- 6.2 Fairness.- 6.3 Transient Predicate.- 6.4 ensures, leads-to.- 6.5 Applications.- 6.6 Theoretical Issues.- 6.7 Concluding Remarks.- 6.8 Bibliographic Notes.- 6.9 Exercises.- 6.10 Solutions to Exercises.- 7 Maximality Properties.- 7.1 Introduction.- 7.2 Notion of Maximality.- 7.3 Proving Maximality.- 7.4 Random Assignment.- 7.5 Fair Unordered Channel.- 7.6 Faulty Channel.- 7.7 Concluding Remarks.- 7.8 Bibliographic Notes.- 8 Program Composition.- 8.1 Introduction.- 8.2 Composition by Union.- 8.3 Examples of Program Union.- 8.4 Substitution Axiom under Union.- 8.5 Theoretical Issues.- 8.6 Concluding Remarks.- 8.7 Bibliographic Notes.- 8.8 Exercises.- 8.9 Solutions to Exercises.- 9 Conditional and Closure Properties.- 9.1 Introduction.- 9.2 Conditional Properties.- 9.3 Closure Properties.- 9.4 Combining Closure and Conditional Properties.- 9.5 Concluding Remarks.- 9.6 Bibliographic Notes.- 10 Reduction Theorem.- 10.1 Introduction.- 10.2 A Model of Seuss Programs.- 10.3 Compatibility.- 10.4 Loose Execution.- 10.5 Reduction Theorem and Its Proof.- 10.6 A Variation of the Reduction Theorem.- 10.7 Concluding Remarks.- 10.8 Bibliographic Notes.- 11 Distributed Implementation.- 11.1 Introduction.- 11.2 Outline of the Implementation Strategy.- 11.3 Design of the Scheduler.- 11.4 Proof of Maximality of the Scheduler.- 11.5 Refining the Scheduling Strategy.- 11.6 Designs of the Processors.- 11.7 Optimizations.- 11.8 Concluding Remarks.- 11.9 Bibliographic Notes.- 12 A Logic for Seuss.- 12.1 Introduction.- 12.2 Specifications of Simple Procedures.- 12.3 Specifications of General Procedures.- 12.4 Persistence and Relative Stability.- 12.5 Strong Semaphore.- 12.6 Starvation Freedom in a Resource Allocation Algorithm.- 12.7 Concluding Remarks.- 12.8 Bibliographic Notes.- In Retrospect.- A Elementary Logic and Algebra.- A.1 Propositional Calculus.- A.2 Predicate Calculus.- A.2.1 Quantification.- A.2.2 Textual substitution.- A.2.3 Universal and Existential quantification.- A.3 Proof Format.- A.4 Hoare Logic and Weakest Pre-conditions.- A.4.1 Hoare logic.- A.4.2 Weakest pre-conditions.- A.5 Elementary Relational Calculus.- References.