Program logic | Logic in computer science | Formal methods
Interference freedom
In computer science, interference freedom is a technique for proving partial correctness ofconcurrent programs with shared variables. Hoare logic had been introduced earlierto prove correctness of sequential programs. In her PhD thesis (and papers arising from it ) under advisor David Gries, Susan Owicki extended this work to apply to concurrent programs. Concurrent programming had been in use since the mid 1960s for coding operating systems as setsof concurrent processes (see, in particular, Dijkstra.), but there was noformal mechanism for proving correctness. Reasoning about interleaved executionsequences of the individual processes was difficult, was error prone,and didn't scale up. Interference freedomapplies to proofs instead of execution sequences;one shows that execution of one process cannot interfere with the correctness proof of another process. A range of intricate concurrent programs have been proved correct using interferencefreedom, and interference freedom provides the basis for much of the ensuing work ondeveloping concurrent programs with shared variables and proving them correct.The Owicki-Gries paper An axiomatic proof technique for parallel programs I received the 1977 ACM Award for best paper in programming languages and systems. Note. Lamport presents a similar idea. He writes, "After writing theinitial version of this paper, we learned of the recent work of Owicki." His paper has not received as much attention as Owicki-Gries, perhaps because it usedflow charts instead of the text of programming constructs like the if statement and while loop.Lamport was generalizing Floyd's method while Owicki-Gries was generalizingHoare's method.Essentially all later work in this area uses text and not flow charts.Another difference is mentioned below in thesection on . (Wikipedia).
