Interference freedom

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 correctness of sequential programs. In her PhD thesis[1] (and papers arising from it [2][3]) 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.[4]), 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 I [2] received the 1977 ACM Award for best paper in programming languages and systems.[5][6]

Note. Lamport [7] presents a similar idea. He writes, "After writing the initial version of this paper, we learned of the recent work of Owicki.[1][2]" 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 [8] while Owicki-Gries was generalizing Hoare's method.[9] Essentially all later work in this area uses text and not flow charts. Another difference is mentioned below in the section on Auxiliary variables.

  1. ^ a b Owicki, Susan S. (August 1975). Axiomatic Proof Techniques for Parallel Programs (PhD thesis). Cornell University. hdl:1813/6393. Retrieved 2022-07-01.
  2. ^ a b c Owicki, Susan; Gries, David (25 June 1976). "An axiomatic proof technique for parallel programs I". Acta Informatica. 6 (4). Berlin: Springer (Germany): 319–340. doi:10.1007/BF00268134. S2CID 206773583.
  3. ^ Owicki, Susan; Gries, David (May 1976). "Verifying properties of parallel programs: an axiomatic approach". Communications of the ACM. 19 (5): 279–285. doi:10.1145/360051.360224. S2CID 9099351.
  4. ^ Dijkstra, E.W. (1968), "The structure of the 'THE'-multiprogramming system", Communications of the ACM, 11 (5): 341–346, doi:10.1145/363095.363143, S2CID 2021311
  5. ^ "Susan S Owicki". Awards.acm.org. Retrieved 2022-07-01.
  6. ^ "David Gries". Awards.acm.org. Retrieved 2022-07-01.
  7. ^ Lamport, Leslie (March 1977). "Proving the correctness of multiprocess programs". IEEE Transactions on Software Engineering. SE-3 (2): 125–143. doi:10.1109/TSE.1977.229904. S2CID 9985552.
  8. ^ Floyd, Robert W. (1967). "Assigning Meanings to Programs" (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32. ISBN 0821867288.
  9. ^ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175.