2046:
1996:, Dijkstra discussed an on-the-fly garbage collector as an exercise in understanding parallelism. The data structure used in a conventional implementation of LISP is a directed graph in which each node has at most two outgoing edges, either of which may be missing: an outgoing left edge and an outgoing right edge. All nodes of the graph must be reachable from a known root. Changing a node may result in unreachable nodes, which can no longer be used and are called
2125:. 2015. Lahav and Vafeiadis strengthen the interference freedom check to produce (we quote from the abstract) "OGRA, a program logic that is sound for reasoning about programs in the release-acquire fragment of the C11 memory model." They provide several examples of its use, including an implementation of the RCU synchronization primitives.
1499:. Write a program that finds the first positive element of an array (if there is one). One process checks all array elements at even positions of the array and terminates when it finds a positive value or when none is found. Similarly, the other process checks array elements at odd positions of the array. Thus, this example deals with
2167:, 1997. Schneider uses interference freedom as the main tool in developing and proving concurrent programs. A connection to temporal logic is given, so arbitrary safety and liveness properties can be proven. Control predicates obviate the need for auxiliary variables for reasoning about program counters.
2211:. Denissen remarks on the ease of use of Dafny and his extension to it, making it extremely suitable when teaching students about interference freedom. Its simplicity and intuitiveness outweighs the drawback of being non-compositional. He lists some twenty institutions that teach interference freedom.
980:
does not occur in the program but is introduced in the proof of correctness to make reasoning simpler —or even possible. Auxiliary variables are used only in assignments to auxiliary variables, so their introduction neither alters the program for any input nor affects the values of program variables.
2229:
2022: This webpage describes the Civl verifier for concurrent programs and gives instructions for installing it on your computer. It is built on top of Boogie, a verifier for sequential programs. Kragl et al describe how interference freedom is achieved in Civl using their new specification idiom,
1678:
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. In this case the assertion is the definition of the bounded buffer and bounds on variables that indicate how many values have
1110:
assertions. 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. Lamport, in his similar work, uses assertions about token positions instead of
259:
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
2137:
extend interference freedom to quantum programming. Difficulties they face include intertwined nondeterminism: nondeterminism involving quantum measurements and nondeterminism introduced by parallelism occurring at the same time. The authors formally verify Bravyi-Gosset-König's parallel quantum
1512:
This example comes from Barry K. Rosen. The solution in Owicki-Gries, complete with program, proof outline, and discussion of interference freedom, takes less than two pages. Interference freedom is quite easy to check, since there is only one shared variable. In contrast, Rosen's article uses
42:
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
2061:
recovers compositionality by abstracting interference into two new predicates in a spec: a rely-condition records what interference a thread must be able to tolerate and a guarantee-condition sets an upper bound on the interference that the thread can inflict on its sibling threads. Xu
2234:. One can also use specs in the rely-guarantee style. Civl offers a combination of linear typing and logic that allows economical and local reasoning about disjointness (like separation logic). Civl is the first system that offers refinement reasoning on structured concurrent programs.
64:
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
1135:
is true of the state upon termination. However, Owicki-Gries also gives some practical techniques that use information obtained from a partial correctness proof to derive other correctness properties, including freedom from deadlock, program termination, and mutual exclusion.
50:
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
115:
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
2241:, and it handles programs operating on the heap using a theory of heaps. A web interface to try it online is available. To handle concurrency, TRICERA uses a variant of the Owicki-Gries proof rules, with explicit variables to added to represent time and clocks.
2114:
as one example. Dongol and Mooij show how to reduce the calculational overhead in formal proofs and derivations and derive Dekker's algorithm again, leading to some new and simpler variants of the algorithm. Mooij studies calculational rules for Unity's
1111:
auxiliary variables, where a token on an edge of a flow chart is akin to a program counter. There is no notion of a history variable. This indicates that Owicki-Gries and
Lamport's approach are not equivalent when restricted to recursive assertions.
1926:
2003:
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.
1166:
show that this new inference rule does not satisfy interference freedom. The fact that the bound function is positive as long as the loop condition is true was not included in an interference test. They show two ways to rectify this mistake.
877:
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
2084:, We quote from: "the Owicki-Gries method involves explicit checking of non-interference between program components, while our system rules out interference in an implicit way, by the nature of the way that proofs are constructed."
96:
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
2010:. Courtois et al use semaphores to give two versions of the readers/writers problem, without proof. Write operations block both reads and writes, but read operations can occur in parallel. Owicki provides a proof.
2066:
observe that Rely-Guarantee is a reformulation of interference freedom; revealing the connection between these two methods, they say, offers a deep understanding about verification of shared variable programs.
2218:
combine the approaches of Hoare-Parallel, a formalisation of Owicki-Gries in
Isabelle/HOL for a simple while-language, and SIMPL, a generic language embedded in Isabelle/HOL, to allow formal reasoning on C
2106:, molded to fit a sequential programming model. Dongel and Goldson describe their logic of progress. Goldson and Dongol show how this logic is used to improve the process of designing programs, using
2000:. An on-the-fly garbage collector has two processes: the program itself and a garbage collector, whose task is to identify garbage nodes and put them on a free list so that they can be used again.
1933:
2226:
introduce the first deductive verification environment in
Isabelle/HOL for C11-like weak memory programs, building on Nipkow and Nieto's encoding of Owicki–Gries in the Isabelle theorem prover.
3382:
Mooij, Arjan J. (November 2007). "Calculating and composing progress properties in terms of the leads-to relation". In
Michael Butler; Michael G. Hinchey; María M. Larrondo-Petrie (eds.).
77:
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
2721:
Apt, Krzysztof R.; de Boer, Frank S.; Olderog, Ernst-Rüdiger (1990). "Proving termination of parallel programs". In Gries, D.; Feijen, W.H.J.; van
Gasteren, A.J.M.; Misra, J. (eds.).
2200:
2005: Ábrahám's PhD thesis provides a way to prove multithreaded Java programs correct in three steps: (1) Annotate the program to produce a proof outline, (2) Use their tool
2090:. 2005-2007. Feijen and van Gasteren show how to use Owicki-Gries to design concurrent programs, but the lack of a theory of progress means that designs are driven only by
3483:
Raad, Azalea; Lahav, Ori; Vafeiadis, Viktor (13 November 2020). "Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86".
2197:
1999: Nipkow and Nieto present the first formalization of interference freedom and its compositional version, the rely-guarantee method, in a theorem prover: Isabelle/HOL.
2031:
The image below, by Ilya Sergey, depicts the flow of ideas that have been implemented in logics that deal with concurrency. At the root is interference freedom. The file
3826:
225:
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.
2187:
provide a systematic and comprehensive introduction to compositional and non-compositional proof methods for the state-based verification of concurrent programs
3656:
de Roever, Willem-Paul; de Boer, Willem-Paul; Hanneman, Ulrich; Hooman, Jozef; Lakhnech, Yassine; Poel, Mannes; Zwiers, Job (2012). Abramsky, S. (ed.).
2045:
2513:
518:} must be provable using some axiom or inference rule of Hoare logic. Thus, the proof outline contains all the information necessary to prove that
2148:
present POG (Persistent Owicki-Gries), the first program logic for reasoning about non-volatile memory technologies, specifically the Intel-x86.
1096:
Instead of using auxiliary variables, one can introduce a program counter into the proof system, but that adds complexity to the proof system.
2237:
2022. Esen and Rümmer developed TRICERA, an automated open-source verification tool for C programs. It is based on the concept of constrained
4012:
3900:
3732:
3640:
3554:
3210:
3120:
2984:
2740:
2138:
algorithm solving a linear algebra problem, giving, they say, for the first time an unconditional proof of a computational quantum advantage.
2076:
supports local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component.
3989:
Kragl, Bernhard; Qadeer, Shaz; Henzinger, Thomas A. (2020). "Refinement for structured concurrent programs". In S. Lahiri; C. Wang (eds.).
47:
instead of execution sequences; one shows that execution of one process cannot interfere with the correctness proof of another process.
4028:
Esen, Zafer; Rümmer, Philipp (October 2022). "TRICERA Verifying C Programs Using the Theory of Heaps". In A. Griggio; N. Rungta (eds.).
3884:
3488:
2204:
to automatically create verification conditions, and (3) Use the theorem prover PVS to prove the verification conditions interactively.
31:
had been introduced earlier to prove correctness of sequential programs. In her PhD thesis (and papers arising from it ) under advisor
4073:
3669:
3395:
3877:
Amani, S.; Andronick, J.; Bortin, M.; Lewis, C.; Rizkallah, C.; Tuong, J. (16 January 2017). Yves Bertot; Viktor
Vafeiadid (eds.).
2161:, 1999. Van Gasteren and Feijen discuss the formal development of concurrent programs entirely on the idea of interference freedom.
3714:
1480:
should be 4. To prove this, because the two assignments are the same, two auxiliary variables are needed, one to indicate whether
3020:
2058:
111:
Construct the individual parts to satisfy their specs, but independent of one another and the context in which they will be used.
1667:
is empty. In Owicki-Gries, a solution in a general environment is shown; it is then embedded in a program that copies an array
1425:. Then the proof outline does not satisfy the requirements, because the assignment contains two occurrences of shared variable
3922:
3767:
3032:
2929:
2664:
2569:
2091:
1162:
loop. It uses a bound function that decreases with each iteration and is positive as long as the loop condition is true. Apt
101:
throughout) of the parts, and not their interior construction. Dijkstra outlined the general steps in using this principle:
2103:
221:
are given that satisfy their specs. But when executing their implementations in parallel, since they share variables, a
1948:
1912:
440:
433:
414:
407:
2077:
1993:
1140:
318:. Two assertions within braces { and } appearing next to each other indicates that the first must imply the second.
3661:
1397:. From this, it is easy to see that these Hoare triples hold. Two similar Hoare triples are required to show that
3443:. ICALP 2015. Lecture Notes in Computer Science. Vol. 9135. Berlin, Heidelberg: Springer. pp. 311–323.
2856:
2809:
2597:
2380:
2564:. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32.
1851:
1816:
3421:
1705:
is an integer variable that can be referenced in only two ways, shown below; each is an indivisible operation:
2207:
2017: Denissen reports on an implementation of Owicki-Gries in the "verification ready" programming language
2119:
relation. Finally, Dongol and Hayes provide a theoretical basis for and prove soundness of the process logic.
618:
With this convention, the only indivisible action need be the memory reference. For example, suppose process
303:
loop.) Hoare alluded to proof outlines in his early work; for interference freedom, it had to be formalized.
4063:
2111:
2015:
1033:, deleting all assignments to them doesn't change the program's correctness, and we have the inference rule
4068:
3841:
3709:
Nipkow, Tobias; Nieto, Leonor Prensa (1999-03-22). "Owicki/Gries in
Isabelle/HOL". In J.P. Finance (ed.).
202:
2897:
558:
164:
3820:
1659:; a consumer process removes them. They proceed at variable rates. The producer must wait if buffer
2110:
for two processes as an example. Dongol and Mooij present more techniques for deriving programs, using
2107:
2019:, a solution to the 2-process mutual exclusion problem, was published by Peterson in a 2-page article.
3843:
Extending Dafny to
Concurrency: Owicki-Gries style program verification for the Dafny program verifier
3027:. 9th IFIP World Computer Congress (Information Processing 83). North-Holland/IFIP. pp. 321–332.
2094:. Dongol, Goldson, Mooij, and Hayes have extended this work to include a "logic of progress" based on
580:
Proving that they work suitably in parallel will require restricting them as follows. Each expression
3620:
3384:
ICFEM'07: Proc. Formal Engineering Methods 9th Int. Conf. on Formal Methods and Software Engineering
2129:
3688:
Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL
1899:
1803:
3951:
3931:
3560:
3463:
3436:
3364:
3265:
3247:
3216:
3071:
2875:
2828:
2746:
2703:
2616:
2530:
2442:
2420:
2399:
2342:
236:
89:
3143:
3686:
4042:
4008:
3896:
3763:
3728:
3665:
3636:
3606:
3550:
3530:
3522:
3391:
3206:
3186:
3116:
3028:
2980:
2956:
2736:
2660:
2565:
2173:, 1991, 2009. This first text to cover verification of structured concurrent programs, by Apt
2020:
2552:
981:
Typically, they are used either as program counters or to record histories of a computation.
27:
is a technique for proving partial correctness of concurrent programs with shared variables.
4037:
3998:
3941:
3888:
3883:. CPP 2017: Proc 6th ACM SIGPLAN Conference on Certified Programs and Proof. Paris, France:
3806:
3789:Ábrahám, Erika; Boer, Frank, S., de; Roever, Willem-Paul, de; Martin, Steffen (2005-02-25).
3755:
3718:
3628:
3542:
3502:
3492:
3462:
Ying, Mingsheng; Zhou, Li; Li, Yangjia (2018). "Reasoning about Parallel Quantum Programs".
3444:
3354:
3323:
3303:
3257:
3198:
3158:
3108:
3092:
3061:
2972:
2938:
2865:
2818:
2780:
2728:
2695:
2686:
2606:
2522:
2432:
2389:
2334:
2325:
2271:
2081:
2073:
232:
213:
are given in terms of their pre- and post-conditions, and we assume that implementations of
108:
Check that the total problem is solved when program parts meeting their specs are available.
20:
2722:
3994:
3616:
3587:
3538:
3387:
3319:
3194:
3104:
2968:
2548:
2033:
1155:
conditions are false. Owicki-Gries provides conditions under which deadlock cannot occur.
74:
3414:
Trace semantics for the Owicki-Gries theory integrated with the progress logic from UNITY
3624:
1970:
is an array of processes that are waiting because they have been suspended; initially,
864:
is part of that indivisible action. If two processes are waiting for the same condition
3342:
2504:
2095:
1697:. In his article on the THE multiprogramming system, Dijkstra introduces the semaphore
222:
61:
2967:. Lecture Notes in Computer Science. Vol. 224. Noordwijkerhout, the Netherlands:
2924:
2655:
Dijkstra, Edsger W. (1982). "EWD 554: A personal summary of the Gries-Owicki Theory".
2459:
1986:. One could change the implementation to always waken the longest suspended process.
4057:
3955:
3658:
Concurrency Verification: Introduction to Compositional and Non-Compositional Methods
3610:
3284:
2942:
2785:
2768:
2620:
2480:
2346:
2181:
Concurrency Verification: Introduction to Compositional and Non-Compositional Methods
2099:
658:
The important innovation of Owicki-Gries was to define what it means for a statement
3916:
Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike (February 2022).
3220:
3075:
2750:
2707:
2634:
806:
Two statements were introduced to deal with concurrency. Execution of the statement
3713:. FASE 1999. Lecture Notes in Computer Science. Vol. 1577. Berlin Heidelberg:
3564:
3368:
2893:
2879:
2847:
2832:
2588:
2534:
2446:
2403:
2367:
2312:
1743:, remove one of the processes from the list of suspended processes associated with
244:
36:
3269:
3261:
3235:
1722:, suspend the process and put it on a list of suspended processes associated with
55:
received the 1977 ACM Award for best paper in programming languages and systems.
4003:
3723:
3448:
3304:"Progress in deriving concurrent programs: emphasizing the role of stable guards"
3096:
2559:
43:
difficult, was error prone, and didn't scale up. Interference freedom applies to
3602:
3579:
3526:
3182:
2800:
2371:
2316:
2238:
868:, when it becomes true, one of them continues waiting while the other proceeds.
281:
240:
124:
32:
28:
3946:
3917:
3412:
3001:
2508:
3811:
3790:
3632:
3546:
3359:
3311:
3202:
3163:
2732:
128:
3878:
3050:"The Rely-Guarantee method for verifying shared variable concurrent programs"
3892:
3751:
An Assertional Proof System for Multithreaded Java - Theory and Tool Support
3003:
Development Methods for Computer Programs including a Notion of Interference
2526:
3507:
2727:. Monographs in Computer Science. New York: Springer Verlag. pp. 0–6.
1488:
has been executed. We leave the change in the proof outline to the reader.
1202: //
678:}, then that proof still holds even in the face of concurrent execution of
2870:
2851:
2823:
2804:
2611:
2592:
2437:
2394:
2375:
3802:
1651:. A producer process generates values and puts them into bounded buffer
4030:
Proc. 22nd Conf. on Formal Methods in Computer-Aided Design – FMCAD 2022
3918:"Integrating Owicki–Gries for C11-Style memory models into Isabelle/HOL"
3327:
2905:(Technical report). Digital Systems Laboratory, Stanford University. 147
4033:
3315:
3066:
2976:
2699:
2338:
3439:. In Halldórsson, M.; Iwama, K.; Kobayashi, N.; Speckmann, B. (eds.).
3285:"Concurrent Program Design in the Extended Theory of Owicki and Gries"
1957:
1883:
1841:
1831:
1787:
3252:
3049:
2960:
2681:
2659:. Monographs in Computer Science. Springer-Verlag. pp. 188–199.
2320:
2275:
1158:
Owicki-Gries presents an inference rule for total correctness of the
732:
Read the last Hoare triple like this: If the state is such that both
3759:
3497:
3112:
1029:
of auxiliary variables are used only in assignments to variables in
608:
at most once. A similar restriction holds for assignment statements
3936:
3880:
COMPLX: A verification framework for concurrent imperative programs
3468:
3308:
MPC'06: Proc. 8th Int. Conf. on Mathematics of Program Construction
3236:"Extending the theory of Owicki and Gries with a logic of progress"
2265:
3969:
3749:
3601:
Apt, Krzysztof R.; Boer, Frank S.; Olderog, Ernst-Rüdiger (2009).
2376:"Verifying properties of parallel programs: an axiomatic approach"
2208:
1385:{(x=0 ∨ x=2) ∧ (x=2 ∨ x=3} S1 {x=2 ∨ x=3}
1380:{(x=0 ∨ x=2) ∧ (x=0 ∨ x=1} S1 {x=0 ∨ x=1}
3291:. Vol. 41. Australian Computer Society, Inc. pp. 41–50.
276:}. It contains all details needed for a proof of correctness of
3343:"Streamlining progress-based derivations of concurrent program"
2769:"Correctness of parallel programs: The Church-Rosser Approach"
2423:(1968), "The structure of the 'THE'-multiprogramming system",
2042:
contains references. Below, we summarize the major advances.
3691:(PhD thesis). Technischen Universitaet Muenchen. p. 198
3289:
CATS '05: Proc 2005 Australasian Symp on Theory of Computing
3246:. Centre pour la Communication Scientifique Directe (CCSD).
2044:
674:
cannot falsify any assertion given in the proof outline of
228:
Thus, Dijkstra's Principle of non-interference is violated.
205:
with shared variables. The specs of two (or more) processes
2049:
Historical graph of program logics for interference freedom
2008:
E. Verification of readers/writers solution with semaphores
1679:
been added to and removed from the buffer. Besides buffer
194:
is true terminates, then upon termination, postcondition
2177:, has gone through several editions over several decades.
1143:
if all processes that have not terminated are executing
3791:"An assertion-based proof system for multithreaded Java"
1102:
Apt discusses the Owicki-Gries logic in the context of
422:
2963:. In J.W. Bakker; W.P. de Roever; G. Rozenberg (eds.).
1520:
An outline of both processes in a general environment:
3993:. Lecture Notes in Computer Science. Vol. 12224.
3048:
Xu, Qiwen; de Roever, Willem-Paul; He, Jifeng (1997).
2899:
Verifying concurrent programs with shared data classes
2657:
Selected Writings on Computing: A Personal Perspective
2321:"An axiomatic proof technique for parallel programs I"
1517:
as the single, running example in this 24 page paper.
3846:(Masters thesis). Eindhoven University of Technology.
2583:
2581:
1119:
Owicki-Gries deals mainly with partial correctness:
3857:
3660:. Cambridge Tracts in Theoretical Computer Science.
2762:
2760:
770:
or assignment statement (that does not appear in an
762:} are interference-free if the following holds. Let
491:
are basic statements, like an assignment statement,
53:
An axiomatic proof technique for parallel programs I
39:
extended this work to apply to concurrent programs.
2057:. 1981. Interference freedom is not compositional.
860:is executed as an indivisible action—evaluation of
506:in the proof outline is preceded by a precondition
3612:Verification of Sequential and Concurrent Programs
3584:Verification of Sequential and Concurrent Programs
3578:Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (1991).
2805:"An exercise in proving parallel programs correct"
2509:"Proving the correctness of multiprocess programs"
2171:Verification of Sequential and Concurrent Programs
3176:
3174:
3087:
3085:
2852:"Concurrent control with "readers" and "writers""
1616:
1343:
1315:
1308:
1301:
1289:
1261:
1254:
1247:
3754:(PhD thesis). Universiteit Leiden. p. 220.
3441:Automata, Languages, and Programming. ICALP 2015
2499:
2497:
2267:Axiomatic Proof Techniques for Parallel Programs
1747:, so its dynamic progress is again permissible.
1089:by deleting all assignments to the variables in
3485:Proceedings of the ACM on Programming Languages
3437:"Owicki-Gries reasoning for weak memory models"
3283:Goldson, Doug; Dongol, Brijesh (January 2005).
3025:Specification and design of (parallel) programs
2362:
2360:
2358:
2356:
1683:itself, two shared variables record the number
1492:Examples of formally proved concurrent programs
596:that can be changed by the other process while
264:Interference freedom in terms of proof outlines
3711:Fundamental Approaches to Software Engineering
2307:
2305:
2303:
2301:
2299:
2297:
2295:
2293:
2291:
2259:
2257:
2255:
1359:{(x=1 ∨ x=3) ∧ (x=2 ∨ x=3)}
1149:statements and none can proceed because their
3302:Dongol, Brijesh; Mooij, Arjan J (July 2006).
3181:Van Gasteren, A.J.M.; Feijen, W.H.J. (1999).
2593:"An axiomatic basis for computer programming"
2415:
2413:
1687:of values added to the buffer and the number
105:Give a complete spec of each individual part.
84:
8:
3825:: CS1 maint: multiple names: authors list (
3615:. Texts in Computer Science (3rd ed.).
3144:"Resources, Concurrency and Local Reasoning"
3097:"Resources, Concurrency and Local Reasoning"
2682:"Recursive assertions and parallel programs"
2635:"Programming Considered as a Human Activity"
885:, then apply the techniques described here.
1649:B. Bounded buffer consumer/producer problem
284:. (This work uses the assignment statement
131:, as exemplified in the specs of processes
3970:"Civl: A verifier for concurrent programs"
3411:Dongol, Brijesh; Hayes, Ian (April 2007).
2925:"Myths about the mutual exclusion problem"
2333:(4). Berlin: Springer (Germany): 319–340.
1868:
1772:
1663:is full; the consumer must wait if buffer
650:, and not some spurious in-between value.
280:} using the axioms and inference rules of
4041:
4002:
3945:
3935:
3810:
3722:
3506:
3496:
3467:
3358:
3251:
3162:
3065:
2869:
2822:
2784:
2610:
2514:IEEE Transactions on Software Engineering
2436:
2393:
2023:and Andrews provide a correctness proof.
3390:, Berlin, Heidelberg. pp. 366–386.
3341:Dongol, Brijesh; Mooij, Arjan J (2008).
3287:. In Mike Atkinson; Frank Dehne (eds.).
3234:Dongol, Brijesh; Goldson, Doug (2006) .
2561:Mathematical Aspects of Computer Science
533:executing in parallel, and their specs:
85:Dijkstra's Principle of non-interference
78:
4043:10.34727/2022/isbn.978-3-85448-053-2_45
3322:, Berlin, Heidelberg. pp. 14–161.
2251:
2192:Implementations of interference freedom
2153:Texts that discuss interference freedom
1393:and the precondition of (2) reduces to
3818:
3537:. Graduate Texts in Computer Science.
3435:Lahav, Ori; Vafeiadis, Viktor (2015).
1484:has been executed; the other, whether
16:Concurrent program verification method
3991:CAV 2020: Computer Aided Verification
2961:"Concepts for concurrent programming"
2112:Peterson's mutual exclusion algorithm
1401:does not interfere with the proof of
1371:does not interfere with the proof of
991:be a set of variables that appear in
824:in parallel. It terminates when both
782:does not interfere with the proof of
700:does not interfere with the proof of
7:
3107:Berlin, Heidelberg. pp. 49–67.
3099:. In P. Gardner; N. Yoshida (eds.).
2027:Dependencies on interference freedom
1375:requires proving two Hoare triples:
725:statement (see later section). Then
3840:Denissen, P.E.J.G (November 2017).
3685:Nieto, Leonor Prensa (2002-01-31).
3240:Logical Methods in Computer Science
1622:
1607:
1590:
1583:
1571:
1555:
1548:
1531:
1389:The precondition of (1) reduces to
1350:
1296:
740:can be executed, then execution of
544:
150:
4036:Academic Press. pp. 360–391.
3193:. Monographs in Computer Science.
3009:(DPhil thesis). Oxford University.
2270:(PhD thesis). Cornell University.
642:must be the value before or after
592:may refer to at most one variable
14:
3101:CONCUR 2004 -- Concurrency Theory
2080:(CSL) was originally proposed by
1701:as a synchronization primitive:
1065:is an auxiliary variable set for
190:in a state in which precondition
2553:"Assigning Meanings to Programs"
2264:Owicki, Susan S. (August 1975).
1990:D. On-the-fly garbage collection
727:{pre-S' ∧ pre-T} T {pre-S'
510:and followed by a postcondition
3191:On A Method Of Multiprogramming
2923:Peterson, Gary L. (June 1981).
2680:Apt, Krzysztof R. (June 1981).
2159:On A Method of Multiprogramming
654:Definition of Interference-free
73:loop. Lamport was generalizing
3923:Journal of Automated Reasoning
2959:; Andrews, Gregory R. (1986).
231:In her PhD thesis of 1975 in
1:
3748:Ábrahám, Erika (2005-01-20).
3586:. Texts in Computer Science.
2965:Current Trends in Concurrency
2846:Courtois, P.J.; Heymans, F.;
1418:statement to the assignment
1226:
1219:
1182:
1177:
1127:executed in a state in which
321:Example: A proof outline for
123:Program specs are written in
94:principle of non-interference
4004:10.1007/978-3-030-53288-8_14
3858:"Dafny Programming Language"
3795:Theoretical Computer Science
3724:10.1007/978-3-540-49020-3_13
3449:10.1007/978-3-662-47666-6_25
3151:Theoretical Computer Science
3023:(1983). R.E.A. Mason (ed.).
2943:10.1016/0020-0190(81)90106-X
2786:10.1016/0304-3975(76)90032-3
2773:Theoretical Computer Science
2088:Deriving concurrent programs
802:Statements cobegin and await
314:and ends with postcondition
268:Owicki-Gries introduced the
3347:Formal Aspects of Computing
3197:New York Inc. p. 370.
3103:. CONCUR 2004. London, UK:
3054:Formal Aspects of Computing
2558:. In Schwartz, J.T. (ed.).
2078:Concurrent separation logic
1994:Summer School Marktoberdorf
1439:statement could be 2 or 3.
852:is delayed until condition
525:Now consider two processes
310:} begins with precondition
4090:
3947:10.1007/s10817-021-09610-2
3662:Cambridge University Press
3306:. In Tarmo Uustalu (ed.).
1695:C. Implementing semaphores
1232:The proof outline for it:
947:{P1} S1 {Q1}, {P2} S2 {Q2}
856:is true. Then, statement
704:} if two conditions hold:
662:not to interfere with the
4074:Logic in computer science
3812:10.1016/j.tcs.2004.09.019
3633:10.1007/978-1-84882-745-5
3547:10.1007/978-1-4612-1830-2
3535:On Concurrent Programming
3360:10.1007/s00165-007-0037-4
3203:10.1007/978-1-4757-3126-2
3164:10.1016/j.tcs.2006.12.035
3000:Jones, C.B. (June 1981).
2857:Communications of the ACM
2810:Communications of the ACM
2733:10.1007/978-1-4612-4476-9
2598:Communications of the ACM
2425:Communications of the ACM
2381:Communications of the ACM
1691:removed from the buffer.
1131:is true terminates, then
475:with every occurrence of
186:Meaning: If execution of
3422:University of Queensland
1175:Consider the statement:
1115:Deadlock and termination
744:is not going to falsify
717:be any statement within
600:is being evaluated, and
247:developed the notion of
239:, written under advisor
3893:10.1145/3018610.3018627
3386:. Boca Raton, Florida:
3262:10.2168/lmcs-2(1:6)2006
3142:O'Hearn, Peter (2007).
2767:Rosen, Barry K (1976).
2527:10.1109/TSE.1977.229904
1468:, so it is the same as
1433:after execution of the
1429:. Indeed, the value of
120:on its implementation.
2724:Beauty is Our Business
2644:. University of Texas.
2642:E. W. Dijkstra Archive
2165:On Current Programming
2050:
1750:The implementation of
1503:loops. It also has no
1472:. After execution of
1346:{Q2: x=2 ∨ x=3}
1292:{Q1: x=1 ∨ x=3}
1108:effectively computable
1016:auxiliary variable set
709:{Q ∧ pre-T} T {Q
203:concurrent programming
3619:London. p. 502.
2871:10.1145/362759.362813
2824:10.1145/359897.359903
2612:10.1145/363235.363259
2438:10.1145/363095.363143
2395:10.1145/360051.360224
2048:
1106:assertions, that is,
995:only in assignments
754:. Proof outlines for
572:
178:
3887:. pp. 138–150.
3717:. pp. 188–203.
3420:(Technical report).
2971:. pp. 669–716.
2016:Peterson's algorithm
1551:add: b:= next value;
1412:is changed from the
888:Inference rules for
622:references variable
483:. (In this example,
306:A proof outline for
299:statements, and the
249:interference freedom
25:interference freedom
3625:2009vscp.book.....A
3328:10.1007/11783596_11
2130:Quantum programming
2092:safety requirements
1069:. The variables in
972:Auxiliary variables
914:{P ∧ B} S {Q}
670:}. If execution of
272:for a Hoare triple
79:Auxiliary variables
3664:USA. p. 800.
3607:Schneider, Fred B.
3531:Schneider, Fred B.
3523:Schneider, Fred B.
3187:Schneider, Fred B.
3067:10.1007/BF01211617
2977:10.1007/BFb0027049
2957:Schneider, Fred B.
2700:10.1007/BF00289262
2339:10.1007/BF00268134
2183:, 2112. De Roever
2108:Dekker's algorithm
2051:
1982:for every process
1446:is changed to the
1311:{x=0 ∨ x=1}
1257:{x=0 ∨ x=2}
978:auxiliary variable
721:but not within an
696:with precondition
237:Cornell University
90:Edsger W. Dijkstra
4014:978-3-030-53288-8
3902:978-1-4503-4705-1
3734:978-3-540-49020-3
3642:978-1-84882-744-8
3556:978-1-4612-1830-2
3491:. pp. 1–28.
3212:978-1-4757-3126-2
3122:978-3-540-28644-8
3093:O'Hearn, Peter W.
2986:978-3-540-16488-3
2803:(December 1977).
2742:978-1-4612-8792-6
1085:is obtained from
949:interference-free
835:Execution of the
832:have terminated.
786:}. Similarly for
467:must hold, where
4081:
4048:
4047:
4045:
4025:
4019:
4018:
4006:
3986:
3980:
3979:
3977:
3976:
3966:
3960:
3959:
3949:
3939:
3913:
3907:
3906:
3874:
3868:
3867:
3865:
3864:
3854:
3848:
3847:
3837:
3831:
3830:
3824:
3816:
3814:
3786:
3780:
3779:
3777:
3776:
3745:
3739:
3738:
3726:
3706:
3700:
3699:
3697:
3696:
3682:
3676:
3675:
3653:
3647:
3646:
3598:
3592:
3591:
3575:
3569:
3568:
3519:
3513:
3512:
3510:
3500:
3480:
3474:
3473:
3471:
3459:
3453:
3452:
3432:
3426:
3425:
3419:
3408:
3402:
3401:
3379:
3373:
3372:
3362:
3338:
3332:
3331:
3310:. Vol. 41.
3299:
3293:
3292:
3280:
3274:
3273:
3255:
3231:
3225:
3224:
3178:
3169:
3168:
3166:
3157:(1–3): 271–307.
3148:
3139:
3133:
3132:
3130:
3129:
3089:
3080:
3079:
3069:
3045:
3039:
3038:
3017:
3011:
3010:
3008:
2997:
2991:
2990:
2953:
2947:
2946:
2920:
2914:
2913:
2911:
2910:
2904:
2890:
2884:
2883:
2873:
2850:(October 1971).
2843:
2837:
2836:
2826:
2797:
2791:
2790:
2788:
2764:
2755:
2754:
2718:
2712:
2711:
2687:Acta Informatica
2677:
2671:
2670:
2652:
2646:
2645:
2639:
2631:
2625:
2624:
2614:
2591:(October 1969).
2585:
2576:
2575:
2557:
2549:Floyd, Robert W.
2545:
2539:
2538:
2501:
2492:
2491:
2489:
2488:
2483:. Awards.acm.org
2477:
2471:
2470:
2468:
2467:
2462:. Awards.acm.org
2460:"Susan S Owicki"
2456:
2450:
2449:
2440:
2417:
2408:
2407:
2397:
2364:
2351:
2350:
2326:Acta Informatica
2319:(25 June 1976).
2309:
2286:
2285:
2283:
2282:
2261:
2232:yield invariants
2074:Separation logic
2041:
2040:
1985:
1981:
1976:
1973:
1969:
1963:
1958:
1954:
1949:
1945:
1940:
1937:
1934:
1930:
1927:
1923:
1913:
1909:
1900:
1896:
1893:
1890:
1884:
1880:
1869:
1865:
1860:
1852:
1848:
1842:
1838:
1832:
1828:
1823:
1820:
1817:
1813:
1804:
1800:
1797:
1794:
1788:
1784:
1773:
1769:
1763:
1757:
1753:
1746:
1742:
1738:
1733:
1725:
1721:
1717:
1712:
1704:
1700:
1690:
1686:
1682:
1674:
1670:
1666:
1662:
1658:
1654:
1645:
1641:
1635:
1632:
1629:
1626:
1623:
1619:
1617:
1611:
1608:
1604:
1591:
1587:
1584:
1579:
1575:
1572:
1568:
1565:
1562:
1559:
1556:
1552:
1549:
1545:
1532:
1528:
1516:
1508:
1487:
1483:
1479:
1475:
1471:
1467:
1464:
1451:
1445:
1438:
1432:
1428:
1424:
1421:
1417:
1411:
1404:
1400:
1396:
1392:
1386:
1381:
1374:
1370:
1364:
1360:
1356:
1351:
1347:
1344:
1340:
1337:
1334:
1331:
1328:
1316:
1312:
1309:
1305:
1302:
1297:
1293:
1290:
1286:
1283:
1280:
1277:
1274:
1262:
1258:
1255:
1251:
1248:
1244:
1237:
1229:
1224:
1217:
1214:
1200:
1197:
1180:
1171:A simple example
1154:
1148:
1139:A program is in
1134:
1130:
1126:
1122:
1092:
1088:
1084:
1080:
1076:
1073:do not occur in
1072:
1068:
1064:
1059:
1058:
1056:
1055:
1052:
1049:
1042:
1036:
1032:
1028:
1021:
1013:
1009:
1005:
1001:
998:
994:
990:
968:
967:
965:
964:
953:
950:
940:
933:
932:
930:
929:
918:
915:
907:
899:
893:
884:
876:
867:
863:
859:
855:
851:
840:
831:
827:
823:
819:
815:
797:
793:
789:
785:
781:
777:
773:
769:
765:
761:
757:
747:
743:
739:
735:
728:
724:
720:
716:
710:
703:
699:
695:
685:
681:
677:
673:
669:
661:
649:
645:
641:
637:
633:
629:
625:
621:
614:
611:
607:
603:
599:
595:
591:
587:
583:
576:
573:
569:
566:
562:
559:
556:
553:
548:
545:
541:
538:
532:
528:
521:
517:
513:
509:
505:
490:
486:
482:
478:
474:
470:
466:
460:
457:
452:
449:
444:
441:
437:
434:
429:
423:
418:
415:
411:
408:
403:
393:
388:
385:
381:
378:
375:
372:
367:
364:
359:
356:
351:
336:
333:
328:
324:
317:
313:
309:
302:
298:
294:
290:
287:
279:
275:
258:
254:
251:. If processes
233:Computer Science
220:
216:
212:
208:
197:
193:
189:
182:
179:
175:
172:
168:
165:
162:
159:
154:
151:
147:
144:
138:
134:
127:, introduced by
21:computer science
4089:
4088:
4084:
4083:
4082:
4080:
4079:
4078:
4054:
4053:
4052:
4051:
4027:
4026:
4022:
4015:
3995:Springer Verlag
3988:
3987:
3983:
3974:
3972:
3968:
3967:
3963:
3915:
3914:
3910:
3903:
3876:
3875:
3871:
3862:
3860:
3856:
3855:
3851:
3839:
3838:
3834:
3817:
3788:
3787:
3783:
3774:
3772:
3770:
3747:
3746:
3742:
3735:
3715:Springer Verlag
3708:
3707:
3703:
3694:
3692:
3684:
3683:
3679:
3672:
3655:
3654:
3650:
3643:
3617:Springer-Verlag
3600:
3599:
3595:
3588:Springer-Verlag
3577:
3576:
3572:
3557:
3539:Springer-Verlag
3521:
3520:
3516:
3498:10.1145/3428219
3487:. Vol. 4.
3482:
3481:
3477:
3461:
3460:
3456:
3434:
3433:
3429:
3417:
3410:
3409:
3405:
3398:
3388:Springer Verlag
3381:
3380:
3376:
3340:
3339:
3335:
3320:Springer Verlag
3301:
3300:
3296:
3282:
3281:
3277:
3233:
3232:
3228:
3213:
3195:Springer-Verlag
3180:
3179:
3172:
3146:
3141:
3140:
3136:
3127:
3125:
3123:
3113:10.1007/b100113
3105:Springer Verlag
3091:
3090:
3083:
3047:
3046:
3042:
3035:
3021:Jones, Cliff B.
3019:
3018:
3014:
3006:
2999:
2998:
2994:
2987:
2969:Springer Verlag
2955:
2954:
2950:
2922:
2921:
2917:
2908:
2906:
2902:
2896:(August 1977).
2892:
2891:
2887:
2864:(10): 667–668.
2845:
2844:
2840:
2817:(12): 921–930.
2799:
2798:
2794:
2766:
2765:
2758:
2743:
2720:
2719:
2715:
2679:
2678:
2674:
2667:
2654:
2653:
2649:
2637:
2633:
2632:
2628:
2605:(10): 576–580.
2589:Hoare, C. A. R.
2587:
2586:
2579:
2572:
2555:
2547:
2546:
2542:
2505:Lamport, Leslie
2503:
2502:
2495:
2486:
2484:
2479:
2478:
2474:
2465:
2463:
2458:
2457:
2453:
2419:
2418:
2411:
2366:
2365:
2354:
2311:
2310:
2289:
2280:
2278:
2263:
2262:
2253:
2248:
2222:2022: Dalvandi
2194:
2155:
2038:
2035:CSL-Family-Tree
2032:
2029:
1983:
1977:
1974:
1971:
1967:
1959:
1956:
1955:
1950:
1947:
1946:
1941:
1938:
1935:
1932:
1931:
1928:
1925:
1924:
1914:
1911:
1910:
1901:
1898:
1897:
1894:
1891:
1885:
1882:
1881:
1870:
1867:
1866:
1863:
1862:
1861:
1853:
1850:
1849:
1843:
1840:
1839:
1833:
1830:
1829:
1824:
1821:
1818:
1815:
1814:
1805:
1802:
1801:
1798:
1795:
1789:
1786:
1785:
1774:
1771:
1770:
1767:
1764:statements is:
1759:
1755:
1751:
1744:
1740:
1736:
1731:
1723:
1719:
1715:
1710:
1702:
1698:
1688:
1684:
1680:
1672:
1668:
1664:
1660:
1656:
1652:
1643:
1642:
1637:
1636:
1633:
1630:
1627:
1624:
1621:
1620:
1615:
1614:
1612:
1609:
1606:
1605:
1592:
1589:
1588:
1585:
1582:
1581:
1577:
1576:
1573:
1570:
1569:
1566:
1563:
1560:
1557:
1554:
1553:
1550:
1547:
1546:
1533:
1530:
1529:
1523:
1514:
1504:
1494:
1485:
1481:
1477:
1473:
1469:
1465:
1453:
1447:
1443:
1434:
1430:
1426:
1422:
1419:
1413:
1409:
1402:
1398:
1394:
1390:
1384:
1382:
1379:
1372:
1368:
1362:
1361:
1358:
1357:
1352:
1349:
1348:
1345:
1342:
1341:
1338:
1335:
1332:
1329:
1317:
1314:
1313:
1310:
1307:
1306:
1303:
1300:
1299:
1295:
1294:
1291:
1288:
1287:
1284:
1281:
1278:
1275:
1263:
1260:
1259:
1256:
1253:
1252:
1249:
1246:
1245:
1239:
1238:
1235:
1227:
1225:
1220:
1218:
1215:
1203:
1201:
1198:
1183:
1181:
1178:
1176:
1173:
1150:
1144:
1132:
1128:
1124:
1120:
1117:
1090:
1086:
1082:
1078:
1074:
1070:
1066:
1062:
1053:
1050:
1047:
1046:
1044:
1043:
1040:
1034:
1030:
1026:
1019:
1011:
1007:
1003:
999:
996:
992:
988:
974:
954:
951:
948:
946:
945:
943:
942:
941:
936:
935:
934:
919:
916:
913:
912:
910:
909:
908:
903:
895:
889:
879:
872:
865:
861:
857:
853:
842:
836:
829:
825:
821:
817:
807:
804:
795:
791:
787:
783:
779:
775:
771:
767:
763:
759:
755:
745:
741:
737:
733:
726:
722:
718:
714:
712:
708:
701:
697:
693:
683:
679:
675:
671:
667:
659:
647:
643:
639:
635:
631:
627:
623:
619:
612:
609:
605:
601:
597:
593:
589:
585:
581:
574:
571:
567:
564:
563:
560:
557:
554:
551:
550:
546:
543:
539:
536:
530:
526:
522:} is correct.
519:
516:{pre-T}T{post-T
515:
511:
507:
503:
502:Each statement
488:
484:
480:
476:
472:
468:
464:
458:
455:
454:
450:
447:
446:
442:
439:
438:
435:
432:
431:
428:{P1 ∧ ¬ e
424:
421:
420:
416:
413:
412:
409:
406:
405:
394:
391:
390:
386:
383:
382:
379:
376:
373:
370:
369:
365:
362:
361:
357:
354:
337:
334:
331:
330:
326:
322:
315:
311:
307:
300:
296:
292:
288:
285:
277:
273:
266:
256:
252:
218:
214:
210:
206:
195:
191:
187:
180:
177:
173:
170:
169:
166:
163:
160:
157:
156:
152:
149:
145:
142:
136:
132:
92:introduced the
87:
17:
12:
11:
5:
4087:
4085:
4077:
4076:
4071:
4066:
4064:Formal methods
4056:
4055:
4050:
4049:
4020:
4013:
3981:
3961:
3908:
3901:
3869:
3849:
3832:
3781:
3768:
3740:
3733:
3701:
3677:
3671:978-0521169325
3670:
3648:
3641:
3593:
3570:
3555:
3541:New York Inc.
3514:
3475:
3454:
3427:
3424:. SSE-2007-02.
3403:
3397:978-3540766483
3396:
3374:
3353:(2): 141–160.
3333:
3294:
3275:
3226:
3211:
3170:
3134:
3121:
3095:(2004-09-03).
3081:
3060:(2): 149–174.
3040:
3033:
3012:
2992:
2985:
2948:
2937:(3): 115–116.
2915:
2885:
2838:
2792:
2779:(2): 183–207.
2756:
2741:
2713:
2694:(3): 219–232.
2672:
2665:
2647:
2626:
2577:
2570:
2540:
2521:(2): 125–143.
2507:(March 1977).
2493:
2472:
2451:
2431:(5): 341–346,
2421:Dijkstra, E.W.
2409:
2388:(5): 279–285.
2352:
2287:
2250:
2249:
2247:
2244:
2243:
2242:
2235:
2227:
2220:
2212:
2205:
2198:
2193:
2190:
2189:
2188:
2178:
2168:
2162:
2154:
2151:
2150:
2149:
2139:
2126:
2120:
2085:
2067:
2055:Rely-Guarantee
2028:
2025:
1992:. At the 1975
1671:into an array
1596:in-out > 0
1578:
1537:in-out < N
1493:
1490:
1172:
1169:
1116:
1113:
1041:
973:
970:
963:{Q1∧Q2}
955:{P1∧P2}
803:
800:
565:
552:
537:
456:
448:
392:
384:
371:
363:
355:
265:
262:
223:race condition
171:
158:
143:
129:Sir Tony Hoare
113:
112:
109:
106:
86:
83:
69:statement and
15:
13:
10:
9:
6:
4:
3:
2:
4086:
4075:
4072:
4070:
4069:Program logic
4067:
4065:
4062:
4061:
4059:
4044:
4039:
4035:
4031:
4024:
4021:
4016:
4010:
4005:
4000:
3996:
3992:
3985:
3982:
3971:
3965:
3962:
3957:
3953:
3948:
3943:
3938:
3933:
3929:
3925:
3924:
3919:
3912:
3909:
3904:
3898:
3894:
3890:
3886:
3882:
3881:
3873:
3870:
3859:
3853:
3850:
3845:
3844:
3836:
3833:
3828:
3822:
3813:
3808:
3804:
3800:
3796:
3792:
3785:
3782:
3771:
3765:
3761:
3757:
3753:
3752:
3744:
3741:
3736:
3730:
3725:
3720:
3716:
3712:
3705:
3702:
3690:
3689:
3681:
3678:
3673:
3667:
3663:
3659:
3652:
3649:
3644:
3638:
3634:
3630:
3626:
3622:
3618:
3614:
3613:
3608:
3604:
3597:
3594:
3589:
3585:
3581:
3574:
3571:
3566:
3562:
3558:
3552:
3548:
3544:
3540:
3536:
3532:
3528:
3524:
3518:
3515:
3509:
3508:10044/1/97398
3504:
3499:
3494:
3490:
3486:
3479:
3476:
3470:
3465:
3458:
3455:
3450:
3446:
3442:
3438:
3431:
3428:
3423:
3416:
3415:
3407:
3404:
3399:
3393:
3389:
3385:
3378:
3375:
3370:
3366:
3361:
3356:
3352:
3348:
3344:
3337:
3334:
3329:
3325:
3321:
3317:
3313:
3309:
3305:
3298:
3295:
3290:
3286:
3279:
3276:
3271:
3267:
3263:
3259:
3254:
3249:
3245:
3241:
3237:
3230:
3227:
3222:
3218:
3214:
3208:
3204:
3200:
3196:
3192:
3188:
3184:
3177:
3175:
3171:
3165:
3160:
3156:
3152:
3145:
3138:
3135:
3124:
3118:
3114:
3110:
3106:
3102:
3098:
3094:
3088:
3086:
3082:
3077:
3073:
3068:
3063:
3059:
3055:
3051:
3044:
3041:
3036:
3030:
3026:
3022:
3016:
3013:
3005:
3004:
2996:
2993:
2988:
2982:
2978:
2974:
2970:
2966:
2962:
2958:
2952:
2949:
2944:
2940:
2936:
2932:
2931:
2926:
2919:
2916:
2901:
2900:
2895:
2894:Owicki, Susan
2889:
2886:
2881:
2877:
2872:
2867:
2863:
2859:
2858:
2853:
2849:
2842:
2839:
2834:
2830:
2825:
2820:
2816:
2812:
2811:
2806:
2802:
2796:
2793:
2787:
2782:
2778:
2774:
2770:
2763:
2761:
2757:
2752:
2748:
2744:
2738:
2734:
2730:
2726:
2725:
2717:
2714:
2709:
2705:
2701:
2697:
2693:
2689:
2688:
2683:
2676:
2673:
2668:
2662:
2658:
2651:
2648:
2643:
2636:
2630:
2627:
2622:
2618:
2613:
2608:
2604:
2600:
2599:
2594:
2590:
2584:
2582:
2578:
2573:
2567:
2563:
2562:
2554:
2550:
2544:
2541:
2536:
2532:
2528:
2524:
2520:
2516:
2515:
2510:
2506:
2500:
2498:
2494:
2482:
2481:"David Gries"
2476:
2473:
2461:
2455:
2452:
2448:
2444:
2439:
2434:
2430:
2426:
2422:
2416:
2414:
2410:
2405:
2401:
2396:
2391:
2387:
2383:
2382:
2377:
2373:
2369:
2368:Owicki, Susan
2363:
2361:
2359:
2357:
2353:
2348:
2344:
2340:
2336:
2332:
2328:
2327:
2322:
2318:
2314:
2313:Owicki, Susan
2308:
2306:
2304:
2302:
2300:
2298:
2296:
2294:
2292:
2288:
2277:
2273:
2269:
2268:
2260:
2258:
2256:
2252:
2245:
2240:
2236:
2233:
2228:
2225:
2221:
2217:
2213:
2210:
2206:
2203:
2199:
2196:
2195:
2191:
2186:
2182:
2179:
2176:
2172:
2169:
2166:
2163:
2160:
2157:
2156:
2152:
2147:
2144:. 2020. Raad
2143:
2140:
2136:
2133:. 2018. Ying
2132:
2131:
2127:
2124:
2121:
2118:
2113:
2109:
2105:
2101:
2097:
2093:
2089:
2086:
2083:
2082:Peter O'Hearn
2079:
2075:
2071:
2068:
2065:
2060:
2056:
2053:
2052:
2047:
2043:
2037:
2036:
2026:
2024:
2022:
2018:
2017:
2011:
2009:
2005:
2001:
1999:
1995:
1991:
1987:
1980:
1964:
1962:
1953:
1944:
1921:
1917:
1908:
1904:
1888:
1879:
1876:
1873:
1859:
1856:
1846:
1836:
1827:
1812:
1808:
1792:
1783:
1780:
1777:
1765:
1762:
1748:
1739:by 1. If now
1734:
1727:
1718:by 1. If now
1713:
1706:
1696:
1692:
1676:
1650:
1646:
1640:
1602:
1599:
1595:
1586:consumer: ...
1543:
1540:
1536:
1527:producer: ...
1526:
1521:
1518:
1510:
1507:
1502:
1498:
1491:
1489:
1462:
1459:
1456:
1450:
1440:
1437:
1416:
1406:
1387:
1376:
1367:Proving that
1365:
1355:
1327:
1324:
1321:
1273:
1270:
1267:
1243:
1233:
1230:
1223:
1212:
1209:
1206:
1195:
1192:
1189:
1186:
1170:
1168:
1165:
1161:
1156:
1153:
1147:
1142:
1137:
1114:
1112:
1109:
1105:
1101:
1097:
1094:
1060:
1038:
1037:elimination:
1023:
1017:
986:
982:
979:
971:
969:
962:
958:
939:
927:
923:
906:
901:
898:
892:
886:
882:
875:
869:
849:
845:
839:
833:
814:
810:
801:
799:
774:) of process
753:
749:
730:
705:
691:
687:
665:
656:
655:
651:
638:receives for
616:
604:may refer to
578:
534:
523:
500:
498:
494:
462:
427:
402:{P1 ∧ e
401:
397:
352:
349:
345:
341:
319:
304:
283:
271:
270:proof outline
263:
261:
250:
246:
242:
238:
234:
229:
226:
224:
204:
201:Now consider
199:
184:
140:
130:
126:
121:
119:
110:
107:
104:
103:
102:
100:
95:
91:
82:
80:
76:
72:
68:
63:
60:
56:
54:
48:
46:
40:
38:
34:
30:
26:
22:
4029:
4023:
3990:
3984:
3973:. Retrieved
3964:
3927:
3921:
3911:
3879:
3872:
3861:. Retrieved
3852:
3842:
3835:
3821:cite journal
3798:
3794:
3784:
3773:. Retrieved
3750:
3743:
3710:
3704:
3693:. Retrieved
3687:
3680:
3657:
3651:
3611:
3603:Gries, David
3596:
3583:
3580:Gries, David
3573:
3534:
3527:Gries, David
3517:
3484:
3478:
3457:
3440:
3430:
3413:
3406:
3383:
3377:
3350:
3346:
3336:
3307:
3297:
3288:
3278:
3253:cs/0512012v3
3243:
3239:
3229:
3190:
3183:Gries, David
3154:
3150:
3137:
3126:. Retrieved
3100:
3057:
3053:
3043:
3024:
3015:
3002:
2995:
2964:
2951:
2934:
2928:
2918:
2907:. Retrieved
2898:
2888:
2861:
2855:
2848:Parnas, D.L.
2841:
2814:
2808:
2801:Gries, David
2795:
2776:
2772:
2723:
2716:
2691:
2685:
2675:
2656:
2650:
2641:
2629:
2602:
2596:
2560:
2543:
2518:
2512:
2485:. Retrieved
2475:
2464:. Retrieved
2454:
2428:
2424:
2385:
2379:
2374:(May 1976).
2372:Gries, David
2330:
2324:
2317:Gries, David
2279:. Retrieved
2266:
2239:Horn clauses
2231:
2223:
2215:
2214:2017: Amani
2201:
2184:
2180:
2174:
2170:
2164:
2158:
2145:
2141:
2134:
2128:
2122:
2116:
2087:
2069:
2063:
2054:
2034:
2030:
2013:
2012:
2007:
2006:
2002:
1997:
1989:
1988:
1978:
1965:
1960:
1951:
1942:
1919:
1915:
1906:
1902:
1886:
1877:
1874:
1871:
1857:
1854:
1844:
1834:
1825:
1810:
1806:
1790:
1781:
1778:
1775:
1766:
1760:
1749:
1729:
1728:
1708:
1707:
1694:
1693:
1677:
1648:
1647:
1638:
1613:this value:=
1600:
1597:
1593:
1541:
1538:
1534:
1524:
1522:
1519:
1511:
1509:statements.
1505:
1500:
1496:
1495:
1460:
1457:
1454:
1448:
1441:
1435:
1414:
1407:
1388:
1377:
1366:
1353:
1325:
1322:
1319:
1271:
1268:
1265:
1241:
1234:
1231:
1221:
1210:
1207:
1204:
1193:
1190:
1187:
1184:
1174:
1163:
1159:
1157:
1151:
1145:
1138:
1123:} means: If
1118:
1107:
1103:
1099:
1098:
1095:
1061:
1039:
1025:Since a set
1024:
1015:
984:
983:
977:
975:
960:
956:
937:
925:
921:
904:
902:
896:
890:
887:
880:
873:
870:
847:
843:
837:
834:
812:
808:
805:
751:
750:
731:
706:
692:. Statement
689:
688:
663:
657:
653:
652:
634:. The value
617:
579:
535:
524:
501:
499:statement.)
496:
492:
479:replaced by
463:
425:
399:
395:
353:
347:
343:
339:
320:
305:
297:if-then-else
269:
267:
248:
245:Susan Owicki
230:
227:
200:
185:
141:
122:
117:
114:
98:
93:
88:
70:
66:
58:
57:
52:
49:
44:
41:
37:Susan Owicki
24:
18:
3930:: 141–171.
3805:: 251–290.
2059:Cliff Jones
1809:sem < 0
1735:: Increase
1714:: Decrease
1452:statement
790:of process
471:stands for
282:Hoare logic
241:David Gries
125:Hoare logic
33:David Gries
29:Hoare logic
4058:Categories
3975:2022-07-22
3937:2004.02983
3863:2022-07-20
3775:2022-07-05
3769:9090189084
3695:2022-07-05
3469:1810.11334
3312:Kuressaare
3128:2022-07-06
3034:0444867295
2909:2022-07-08
2666:0387906525
2571:0821867288
2487:2022-07-01
2466:2022-07-01
2281:2022-07-01
2246:References
1720:sem < 0
1497:A. Findpos
1054:{P} S {Q}
1048:{P} S' {Q}
985:Definition
841:statement
752:Definition
690:Definition
3956:215238874
2621:207726175
2347:206773583
2276:1813/6393
2219:programs.
2102:language
2021:Schneider
1104:recursive
816:executes
811:S1 // S2
796:{P1}S1{Q1
784:{P2}S2{Q2
760:{P2}S2{Q2
756:{P1}S1{Q1
198:is true.
3803:Elsevier
3760:1887/584
3609:(eds.).
3590:Germany.
3533:(eds.).
3525:(1997).
3221:13607884
3189:(eds.).
3076:12148448
2751:24379938
2708:42470032
2551:(1967).
2117:leads-to
2072:. 2004.
1905:sem ≤ 0
1655:of size
1625:markout:
1442:Suppose
1408:Suppose
1141:deadlock
1121:{P} S {Q
1002:, where
778:. Then
713:(2) Let
646:changes
630:changes
575:{post-S2
568:{post-S1
495:, or an
325:} where
323:{P} S {Q
174:{post-S1
4034:TU Wien
3801:(2–3).
3621:Bibcode
3582:(ed.).
3565:9980317
3369:7024064
3316:Estonia
2880:7540747
2833:3202388
2535:9985552
2447:2021311
2404:9099351
2100:Misra's
1998:garbage
1929:that w;
1918:choose
1864:V(sem):
1768:P(sem):
1741:sem ≤ 0
1610:remove:
1558:markin:
1525:cobegin
1515:Findpos
1436:cobegin
1242:cobegin
1185:cobegin
1057:
1045:
1010:. Then
966:
959:S1//S2
957:cobegin
944:
938:cobegin
931:
911:
897:cobegin
809:cobegin
547:{pre-S2
540:{pre-S1
514:, and
293:if-then
196:post-Si
181:{pre-S2
153:{pre-S2
146:{pre-S1
75:Floyd's
62:Lamport
4011:
3954:
3899:
3766:
3731:
3668:
3639:
3563:
3553:
3394:
3367:
3270:302420
3268:
3219:
3209:
3119:
3074:
3031:
2983:
2878:
2831:
2749:
2739:
2706:
2663:
2619:
2568:
2533:
2445:
2402:
2345:
2202:Verger
2096:Chandy
1966:Here,
1895:sem+1;
1799:sem-1;
1758:using
1732:V(sem)
1711:P(sem)
1634:out+1;
1363:{x=3}
1304:{x=0}
1250:{x=0}
1236:{x=0}
1228:{x=3}
1179:{x=0}
1014:is an
1006:is in
987:. Let
928:S {Q}
766:be an
758:} and
746:pre-S'
702:{P}S{Q
676:{P}S{Q
668:{P}S{Q
626:while
520:{P}S{Q
512:post-T
465:P ⇒ P1
308:{P}S{Q
278:{P}S{Q
274:{P}S{Q
260:more.
192:pre-Si
45:proofs
3952:S2CID
3932:arXiv
3561:S2CID
3464:arXiv
3418:(PDF)
3365:S2CID
3266:S2CID
3248:arXiv
3217:S2CID
3147:(PDF)
3072:S2CID
3007:(PDF)
2903:(PDF)
2876:S2CID
2829:S2CID
2747:S2CID
2704:S2CID
2638:(PDF)
2617:S2CID
2556:(PDF)
2531:S2CID
2443:S2CID
2400:S2CID
2343:S2CID
2224:et al
2216:et al
2209:Dafny
2185:et al
2175:et al
2146:et al
2135:et al
2104:Unity
2064:et al
2039:(PDF)
1979:false
1943:false
1916:begin
1887:begin
1872:await
1845:await
1791:begin
1776:await
1761:await
1639:coend
1594:await
1567:in+1;
1535:await
1506:await
1501:while
1466:= x+2
1455:await
1449:await
1423:= x+1
1415:await
1354:coend
1320:await
1266:await
1222:coend
1216:= x+2
1205:await
1199:= x+1
1188:await
1164:et al
1160:while
1152:await
1146:await
1100:Note:
961:coend
922:await
905:await
900:are:
891:await
881:await
874:await
844:await
838:await
813:coend
772:await
768:await
723:await
698:pre-T
664:proof
508:pre-T
497:await
338:= a;
301:while
118:never
99:specs
71:while
59:Note.
4009:ISBN
3897:ISBN
3827:link
3764:ISBN
3729:ISBN
3666:ISBN
3637:ISBN
3551:ISBN
3392:ISBN
3207:ISBN
3117:ISBN
3029:ISBN
2981:ISBN
2737:ISBN
2661:ISBN
2566:ISBN
2519:SE-3
2123:OGRA
2098:and
1922:such
1907:then
1889:sem:
1878:then
1875:true
1858:skip
1855:then
1826:true
1811:then
1793:sem:
1782:then
1779:true
1754:and
1628:out:
1601:skip
1598:then
1542:skip
1539:then
1461:then
1458:true
1383:(2)
1378:(1)
1326:then
1323:true
1318:S2:
1272:then
1269:true
1264:S1:
1211:then
1208:true
1194:then
1191:true
1018:for
926:then
920:{P}
894:and
871:The
848:then
828:and
820:and
794:and
736:and
707:(1)
682:and
529:and
493:skip
487:and
426:else
400:then
380:= a;
348:else
344:then
295:and
255:and
217:and
209:and
135:and
4038:doi
3999:doi
3942:doi
3889:doi
3885:ACM
3807:doi
3799:331
3756:hdl
3719:doi
3629:doi
3543:doi
3503:hdl
3493:doi
3489:ACM
3445:doi
3355:doi
3324:doi
3258:doi
3199:doi
3159:doi
3155:375
3109:doi
3062:doi
2973:doi
2939:doi
2930:IPL
2866:doi
2819:doi
2781:doi
2729:doi
2696:doi
2607:doi
2523:doi
2433:doi
2390:doi
2335:doi
2272:hdl
2142:POG
2070:CSL
2014:F.
1961:end
1952:end
1835:end
1745:sem
1737:sem
1730:2.
1724:sem
1716:sem
1709:1.
1703:sem
1699:sem
1689:out
1644:...
1574:...
1561:in:
1395:x=2
1391:x=0
1339:x+2
1285:x+1
1240:S:
1077:or
1000:= E
976:An
798:}.
729:}.
666:of
613:= E
588:or
584:in
451:{Q1
443:{Q1
417:{Q1
387:{P1
366:{P1
346:S1
329:is:
289:= e
19:In
4060::
4032:.
4007:.
3997:.
3950:.
3940:.
3928:66
3926:.
3920:.
3895:.
3823:}}
3819:{{
3797:.
3793:.
3762:.
3727:.
3635:.
3627:.
3605:;
3559:.
3549:.
3529:;
3501:.
3363:.
3351:20
3349:.
3345:.
3318::
3314:,
3264:.
3256:.
3242:.
3238:.
3215:.
3205:.
3185:;
3173:^
3153:.
3149:.
3115:.
3084:^
3070:.
3056:.
3052:.
2979:.
2935:12
2933:.
2927:.
2874:.
2862:14
2860:.
2854:.
2827:.
2815:20
2813:.
2807:.
2775:.
2771:.
2759:^
2745:.
2735:.
2702:.
2692:15
2690:.
2684:.
2640:.
2615:.
2603:12
2601:.
2595:.
2580:^
2529:.
2517:.
2511:.
2496:^
2441:,
2429:11
2427:,
2412:^
2398:.
2386:19
2384:.
2378:.
2370:;
2355:^
2341:.
2329:.
2323:.
2315:;
2290:^
2254:^
1936:w:
1903:if
1847:¬w
1819:w:
1807:if
1726:.
1685:in
1675:.
1618:b;
1580://
1486:S2
1482:S1
1476:,
1470:S2
1463:x:
1444:S1
1420:x:
1410:S1
1405:.
1403:S1
1399:S2
1373:S2
1369:S1
1298://
1213:x:
1196:x:
1093:.
1091:AV
1087:S'
1081:.
1071:AV
1067:S'
1063:AV
1035:AV
1031:AV
1027:AV
1022:.
1020:S'
1012:AV
1008:AV
997:x:
993:S'
989:AV
924:B
846:B
830:S2
826:S1
822:S2
818:S1
792:S2
776:S1
748:.
738:S'
715:S'
686:.
644:S2
636:S1
628:S2
620:S1
615:.
610:x:
590:S2
586:S1
577:}
561:S2
555:S1
531:S2
527:S1
489:S2
485:S1
473:P1
469:P1
461:}
459:{Q
436:S2
410:S1
398:e
396:if
358:{P
350:S2
342:e
340:if
291:,
286:x:
257:S2
253:S1
243:,
235:,
219:S2
215:S1
211:S2
207:S1
188:Si
183:}
167:S2
161:S1
139::
137:S2
133:S1
81:.
67:if
35:,
23:,
4046:.
4040::
4017:.
4001::
3978:.
3958:.
3944::
3934::
3905:.
3891::
3866:.
3829:)
3815:.
3809::
3778:.
3758::
3737:.
3721::
3698:.
3674:.
3645:.
3631::
3623::
3567:.
3545::
3511:.
3505::
3495::
3472:.
3466::
3451:.
3447::
3400:.
3371:.
3357::
3330:.
3326::
3272:.
3260::
3250::
3244:2
3223:.
3201::
3167:.
3161::
3131:.
3111::
3078:.
3064::
3058:9
3037:.
2989:.
2975::
2945:.
2941::
2912:.
2882:.
2868::
2835:.
2821::
2789:.
2783::
2777:2
2753:.
2731::
2710:.
2698::
2669:.
2623:.
2609::
2574:.
2537:.
2525::
2490:.
2469:.
2435::
2406:.
2392::
2349:.
2337::
2331:6
2284:.
2274::
1984:p
1975:=
1972:w
1968:w
1939:=
1920:p
1892:=
1837:;
1822:=
1796:=
1756:V
1752:P
1681:b
1673:d
1669:c
1665:b
1661:b
1657:N
1653:b
1631:=
1603:;
1564:=
1544:;
1478:x
1474:S
1431:x
1427:x
1336:=
1333::
1330:x
1282:=
1279::
1276:x
1133:Q
1129:P
1125:S
1083:S
1079:Q
1075:P
1051:/
1004:x
952:/
917:/
883:s
866:B
862:B
858:S
854:B
850:S
788:T
780:T
764:T
742:T
734:T
719:S
711:}
694:T
684:T
680:S
672:T
660:T
648:y
640:y
632:y
624:y
606:y
602:E
598:E
594:y
582:E
570:}
549:}
542:}
504:T
481:a
477:x
453:}
445:}
430:}
419:}
404:}
389:}
377::
374:x
368:}
360:}
335::
332:x
327:S
316:Q
312:P
176:}
155:}
148:}
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
