Specifying Distributed Systems


Butler Lampson


Citation: Constructive Methods in Computer Science, ed. M. Broy, NATO ASI Series F: Computer and Systems Sciences 55, Springer, 1989, pp 367-396.

Links: Abstract, Acrobat. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.

Email: blampson@microsoft.com. This paper is at http://research.microsoft.com.



These notes describe a method for specifying concurrent and distributed systems, and illustrate it with a number of examples, mostly of storage systems. The specification method is due to Lamport, and the notation is an extension, due to Nelson, of Dijkstra’s guarded commands.