In computer science, interference freedom is a technique for proving partial correctness of concurrent programs with shared variables. Hoare logic had been introduced earlier to prove the 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 sets of concurrent processes (see, in particular, Dijkstra.), but there was no formal mechanism for proving correctness. Reasoning about interleaved execution sequences of the individual processes was difficult, was error prone, and didn't scale up. Interference freedom applies 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 interference freedom, and interference freedom provides the basis for much of the ensuing work on developing concurrent programs with shared variables and proving them correct. The Owicki-Gries paper An axiomatic proof technique for parallel programs received the 1977 ACM Award for best paper in programming languages and systems. Note. Lamport presents a similar idea. He writes, "After writing the initial 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 used flow 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 generalizing Hoare's method. Essentially, all later work in this area uses text and not flow charts. Another difference is mentioned below in the section on Auxiliary variables.
Dijkstra's Principle of non-interference Edsger W. Dijkstra introduced the principle of non-interference in EWD 117, "Programming Considered as a Human Activity", written about 1965. This principle states that: The correctness of the whole can be established by taking into account only the exterior specifications (abbreviated specs throughout) of the parts, and not their interior construction. Dijkstra outlined the general steps in using this principle:
Give a complete spec of each individual part. Check that the total problem is solved when program parts meeting their specs are available. Construct the individual parts to satisfy their specs, but independent of one another and the context in which they will be used. He gave several examples of this principle outside of programming. But its use in programming is a main concern. For example, a programmer using a method (subroutine, function, etc.) should rely only on its spec to determine what it does and how to call it, and never on its implementation. Program specs are written in Hoare logic, introduced by Sir Tony Hoare, as exemplified in the specs of processes S1 and S2: {pre-S1} {pre-S2} S1 S2 {post-S1} {pre-S2} Meaning: If execution of Si in a state in which precondition pre-Si is true terminates, then upon termination, postcondition post-Si is true. Now consider concurrent programming with shared variables. The specs of two (or more) processes S1 and S2 are given in terms of their pre- and post-conditions, and we assume that implementations of S1 and S2 are given that satisfy their specs. But when executing their implementations in parallel, since they share variables, a race condition can occur; one process changes a shared variable to a value that is not anticipated in the proof of the other process, so the other process does not work as intended. Thus, Dijkstra's Principle of non-interference is violated. In her PhD thesis of 1975 in Computer Science, Cornell University, written under advisor David Gries, Susan Owicki developed the notion of interference freedom. If processes S1 and S2 satisfy interference freedom, then their parallel execution will work as planned. Dijkstra called this work the first significant step toward applying Hoare logic to concurrent processes. To simplify discussions, we restrict attention to only two concurrent processes, although Owicki-Gries allows more.
… excerpt ends here. Continue reading the full article.
