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.

Reasoning about interleaved execution sequences of the individual processes was difficult, was error prone, and didn't scale up.

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.

[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.

Edsger W. Dijkstra introduced the principle of non-interference in EWD 117, "Programming Considered as a Human Activity", written about 1965.

[10] 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.

Program specs are written in Hoare logic, introduced by Sir Tony Hoare,[9] 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.

In her PhD thesis of 1975 [1] in Computer Science, Cornell University, written under advisor David Gries, Susan Owicki developed the notion of interference freedom.

Dijkstra called this work the first significant step toward applying Hoare logic to concurrent processes.

It contains all details needed for a proof of correctness of {P}S{Q} using the axioms and inference rules of Hoare logic.

Hoare alluded to proof outlines in his early work; for interference freedom, it had to be formalized.

A similar restriction holds for assignment statements x:= E. With this convention, the only indivisible action need be the memory reference.

Definition of Interference-free The important innovation of Owicki-Gries was to define what it means for a statement T not to interfere with the proof of {P}S{Q}.

The await statement cannot be implemented efficiently and is not proposed to be inserted into the programming language.

Rather it provides a means of representing several standard primitives such as semaphores—first express the semaphore operations as awaits, then apply the techniques described here.

He proves that all the assertions in proof outlines can be recursive, but that this is no longer the case if auxiliary variables are used only as program counters and not to record histories of computation.

It uses a bound function that decreases with each iteration and is positive as long as the loop condition is true.

The fact that the bound function is positive as long as the loop condition is true was not included in an interference test.

Then the proof outline does not satisfy the requirements, because the assignment contains two occurrences of shared variable x.

[14] The solution in Owicki-Gries,[2] complete with program, proof outline, and discussion of interference freedom, takes less than two pages.

In contrast, Rosen's article[14] uses Findpos as the single, running example in this 24 page paper.

An outline of both processes in a general environment: cobegin producer: ... await in-out < N then skip; add: b[in mod N]:= next value; markin: in:= in+1; ... // consumer: ... await in-out > 0 then skip; remove: this value:= b[out mod N]; markout: out:= out+1; coend ... B. Bounded buffer consumer/producer problem.

This example exhibits a principle to reduce interference checks to a minimum: Place as much as possible in an assertion that is invariantly true everywhere in both processes.

At the 1975 Summer School Marktoberdorf, Dijkstra discussed an on-the-fly garbage collector as an exercise in understanding parallelism.

Gries felt that interference freedom could be used to prove the on-the-fly garbage collector correct.

With help from Dijkstra and Hoare, he was able to give a presentation at the end of the Summer School, which resulted in an article in CACM.

[19] The image below, by Ilya Sergey, depicts the flow of ideas that have been implemented in logics that deal with concurrency.