A semantic model for parallel systems with scheduling

ABSTRACT

This paper presents a semantic model for parallel systems with a scheduling mechanism that is useful for expressing and proving a wider range of properties than semantic models that do not consider scheduling.We formally describe a number of properties related to scheduling and deadlock, including "Fairness" and "Fullness", and show that schedulers with these properties behave in desirable ways.Lastly, we prove and conjecture some proof rules for scheduled systems and outline briefly the relation of this work to modelling protection in parallel systems.

REFERENCES

• 1: {Cadiou & Levy 73} Cadiou, J., J. Levy, "Mechanizable proofs about Parallel Processes," 14th Symposium on Switching Theory and Automata, October, 1973.
• 2: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 3: {Cohen 74} Cohen, E., Semantic Models for Parallel Systems, CMU Tech. Report, December, 1974.
• 4: {Cohen 75} Cohen, E., Modelling Protection Systems, CMU Ph.D Thesis, forthcoming.
• 5: {Dijkstra 72} Dijkstra, E., "A Class of Allocation Strategies Inducing Bounded Delay Only," SJCC 72.
• 6: {Kahn 73} Kahn, G., A Preliminary Theory for Parallel Programs, I.R.I.A. Report, January, 1973.
• 7: Richard J. Lipton, On synchronization primitive systems, 1973
• 8: Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972 [doi>10.1145/361454.361460]
• 9: {Milner 71} Milner, R., "An Algebraic Definition of Simulation between Programs," I.J.C.A.I. 2, 1971.
• 10: Robin Milner, Implementation and applications of Scott's logic for computable functions, Proceedings of ACM conference on Proving assertions about programs, p.1-6, January 06-07, 1972, Las Cruces, New Mexico, United States
• 11: {Milner & Weyrauch 72} Milner, R. and R. Weyrauch, "Proving Compiler Correctness in a Mechanized Logic," Machine Intelligence 7.
• 12: Malcolm C. Newey, Axioms and theorems for integers, lists and finite sets in LCF., Stanford University, Stanford, CA, 1973
• 13: {Rotenberg 74} Rotenberg, L., Making Computers Keep Secrets, MIT Ph.D Thesis, MAC TR 115, February, 1974.
• 14: {Scott 72} Scott, D., "The Lattice of Flow Diagrams," Symp. on Semantics of Algorithmic Languages, Springer Verlag Lecture Notes in Mathematics 188, 1971.
• 15: {Scott 72} Scott, D., "Mathematical Concepts in Programming Language Semantics," SJCC 72.
• 16: {Scott & Strachey 72} Scott, D., C. Strachey, Toward a Mathematical Semantics for Computer Languages, Oxford University Computing Lab PRG-6, 1972.