SRC Research Report 44

Pretending Atomicity.

Leslie Lamport and Fred B.~Schneider.

We present a theorem for deriving properties of a concurrent program by reasoning about a simpler, coarser-grained version. The theorem generalizes a result that Lipton proved for partial correctness and deadlock-freedom. Our theorem applies to all safety properties.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 120 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 96 Kbytes
  
• PostScript compressed with ZIP -- 96 Kbytes
  
• PostScript -- 240 Kbytes
  
• Portable Document Format (PDF) -- 232 Kbytes