Microsoft Research Blog

English

  3. The Weak Byzantine Generals Problem 

    June 7, 1983 | Leslie Lamport

    This paper introduces a weaker version of the Byzantine generals problem described in [41]. The problem is "easier" because there exist approximate solutions with fewer than 3n processes that can tolerate n faults, something shown in [41] to be impossible for the original Byzantine generals…

  4. Organizing software in a distributed environment 

    June 1, 1983 | Butler Lampson and Eric Schmidt

    The System Modeller provides automatic support for several different kinds of program development cycle in the Cedar programming system. It handles the daily evolution of a single module or a small group of modules modified by a single person, the assembly of numerous modules into…

  5. What Good Is Temporal Logic? 

    May 5, 1983 | Leslie Lamport

    This was an invited paper. It describes the state of my views on specification and verification at the time. It is notable for introducing the idea of invariance under stuttering and explaining why it's a vital attribute of a specification logic. It is also one…

  6. Lattice Yang-Mills Theory at Nonzero Temperature and the Confinement Problem 

    May 3, 1983 | Christian Borgs and Erhard Seiler

    We discuss finite temperature lattice Yang-Mills theory with special attention to the confinement problem. The relationship between the confinement criteria of Wilson, Polyakov, and 't Hooft is clarified by establishing a string of inequalities between the corresponding string tensions. The close connection between finite temperature…

  8. Specifying Concurrent Program Modules 

    April 5, 1983 | Leslie Lamport

    The early methods for reasoning about concurrent programs dealt with proving that a program satisfied certain properties--usually invariance properties. But, proving particular properties showed only that the program satisfied those properties. There remained the possibility that the program was incorrect because it failed to satisfy…

  9. Reasoning About Nonatomic Operations 

    January 1, 1983 | Leslie Lamport

    From the time I discovered the bakery algorithm (see [12]), I was fascinated by the problem of reasoning about a concurrent program without having to break it into indivisible atomic actions. In [33], I described how to do this for behavioral reasoning. But I realized…

  10. Topological Charge Distribution in SU(N) Gauge Theories 

    January 1, 1983 | Christopher Bishop and P. V. D. Swift

    The probability distribution function for topological charge contained in a sphere of finite radius is calculated. We find no need to introduce an arbitrary cutoff on instanton scale sizes as this is controlled by the size of the sphere. Recent Monte Carlo calculations reflect qualitatively…

  11. An Assertional Correctness Proof of a Distributed Program 

    December 5, 1982 | Leslie Lamport

    I showed in [27] that there is no invariant way of defining the global state of a distributed system. Assertional methods, such as [23], reason about the global state. So, I concluded that these methods were not appropriate for reasoning about distributed systems. When I…

  12. A laser rangefinder for robot control and inspection 

    November 1, 1982 | Sarangarajan Parthasarathy, J. Birk, and J. Dessimoz

    Three-dimensional surface point data is often useful for r0b0t control and inspection casks. The design of sensors for collecting this data involves many choices, with selections made on the basis of data rate, accuracy, field of view, safety, size, object properties, and the need for…