The Correctness of the PACLIB Kernel

A Case Study in Parallel Program Verification by Temporal Logic^{∗}

Wolfgang Schreiner Research Institute for Symbolic Computation (RISC-Linz) Johannes Kepler University, Linz, Austria

           email: schreine@risc.uni-linz.ac.at

April 20, 1993

Abstract

We verify the correct implementation of a non-deterministic construct for the delivery of task results in the parallel computer algebra library Paclib. First we explain the corresponding part of the Paclib runtime kernel. Then we give an overview on the calculus of temporal logic and extend it for our purposes. We describe how the Paclib kernel is modelled in this formal framework. We formulate several key theorems and auxiliary lemmas that capture the dynamic behavior of the construct and verify their correctness. Based on the experiences of this case study, we describe some general verification strategies.

∗Supported by the FWF grant S5302-PHY “Parallel Symbolic Computation”.

Contents

1 Introduction 4

2 Parallel Program Verification 5 2.1 Organization of the Verification . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Program Model and Implementation . . . . . . . . . . . . . . . . . . . . . . 6 2.3 The Complexity of Verification . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 The Purpose of Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.5 The Role of the Parallel Programming Model . . . . . . . . . . . . . . . . . 8

3 The PACLIB Kernel 8 3.1 The Programming Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.2 Task Creation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.3 Task Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.4 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.5 Verification Goal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

4 Temporal Logic and the Semantics of Programs 13 4.1 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Parallel Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.3 Program Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.4 Temporal Program Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.5 Description of Program Properties . . . . . . . . . . . . . . . . . . . . . . . 20 4.6 Time Constants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

5 The Formal Model 25 5.1 The Overall Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.2 The Correctness Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 5.3 The Detailed Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

6 The Verification 32 6.1 No Result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 6.2 Result Delivery . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

6.2.1 Case τr → △β{j \atop 23} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

6.2.2 Case τ → △β{j \atop 24} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

6.3 Wait Continuation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

7 Conclusions 39 A The PACLIB Kernel 43

B Lemmas 46 B.1 Mutual Exclusion Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 B.2 Operation Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 B.3 Structure Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 B.4 Main Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 B.5 Continuation Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

C The Program Model 67

Beware of bugs in the above code; I’ve only proved it correct, not tried it.

Donald Knuth

1 Introduction

The verification of parallel programs is a very complicated and tedious task. The more freedom a programming language provides for inter-process communication and synchronization, the more complex the interaction between parallel processes may become, the more error-prone a program is and the more issues a verification has to consider. One of the most difficult cases is that of a program where many processes are tightly coupled by shared memory and synchronized by semaphores or equivalent constructs.

High-level parallel programming languages therefore offer more restricted forms of communication and synchronization that yield less error-prone programs whose correctness may be verified more easily. However, the implementation of a high-level parallel programming construct is based on low-level concepts; its verification is therefore a difficult task in its own. One reason for this is that the correctness of a language construct has to be established for every program that applies the construct!

In this paper, we will verify the correct implementation of the non-deterministic function pacWait that is used in the parallel computer algebra library Paclib [HSN^{+}92] for the delivery of task results. Paclib programs using pacWait are quite loosely coupled and their verification is in general rather easy (i.e. the correctness of the parallel program can be essentially reduced to the correctness of the sequential program). However, the implementation of pacWait itself demands a complicated interaction of tightly coupled parallel processes. The pacWait algorithm is relatively short, but its dynamical behavior makes a verification rather difficult.

There exist several calculi for the formal verification of parallel programs e.g. the axiomatic model by [OG76, OL82], the Unity model [CM88], Millner’s CCS [Mil80], the Π-calculus [Mil93], Hoare’s CSP [Hoa85] or temporal logic [MP81, Krö87]. The introduction of these calculi usually consists of the proof of their mathematical soundness and completeness and their application to small example programs.

However, techniques that may be useful for the verification of small programs may fail for more realistic examples. The reason for this are not mathematical deficiencies but pragmatic ones, for instance if the complexity of verification is prohibitive. Therefore, realistic examples are necessary not only to evaluate the practical usefulness of a calculus but also to suggest adaptations and modifications that may increase its range of application. Unfortunately, there are only few such examples in literature [Oss83].

The goal of this paper is to present the verification of a parallel program with a rather complex dynamical behavior whose correctness is not immediately clear. We do not start the verification with a nice formal model but first present the “real-world” problem that we actually want to be solved, then show how this problem can be modelled in a formal framework and finally derive the properties of this model.

The next section of this paper contains several “meta-remarks” on the issue of parallel program verification, its usefulness and its limitations. The main components of the case study are then presented in the following sections:

1. the description of pacWait and its implementation,

2. the framework of temporal logic,

3. the formal model and the correctness theorem, and

4. the verification itself.

Some general strategies for parallel program verification derived from our case study conclude the paper. The appendix contains the source code of the actual program and the proofs of the lemmas used in the verification.

\underline{5}

2 Parallel Program Verification

In this section, we will present our view on the formal verification of parallel programs, its usefulness and its limitations. We will argue that

1. The goal of parallel program verification is to increase the confidence in some properties of an executable parallel program.

2. However, the formal verification process is only able to deal with a reduced model of this program.

3. The adequacy of the model with respect to the interesting properties of the real program cannot be checked by formal methods.

4. Even a formal verification of the model in general extremely complex and only feasible by radical simplifications.

5. Parallel program verification is therefore as error-prone as parallel programming itself and its adequacy cannot be guaranteed.

6. The importance of parallel program verification is that of documenting a parallel program more than of proving it.

The section is rather (maybe too) lengthy and mainly contains the personal options of the author. The hasty reader only interested in the formal part of this paper may therefore skip it and directly go the next section.

2.1 Organization of the Verification

The process of program verification consists in our opinion of the following components:

1. A Running Program: There is given a program p that has in all past test runs shown the desired behavior. However, the programmer would like to increase his confidence that the program will show this behavior for all future runs (and all given inputs) and/or convince other people of this fact. For this purpose, informal reasoning in a natural language is by its ambiguity not considered sufficient.

2. A Formal Framework: The programmer chases a framework that allows more precisely than natural language to express properties of the program and to reason about these properties. To simplify the reasoning, this framework is a reduced image of the “real world” (i.e. computer hardware, operating system, programming language) neglecting all effects that the programmer considers of minor importance for the aspects of the program he is interested in. By the formal structure of the model, the correctness of the reasoning process can be more easily controlled.

3. Program Model: In the chosen framework, the programmer constructs a model p̄ of the program and a proposition cp̄ that describes the notion of “correctness” in this model. If for each possible “model run” r of p̄ the proposition cp̄(r) holds, the program is considered correct. If a single counterexample r′ with ¬cp̄(r′) can be constructed, the program is considered incorrect. However, the question whether p̄ and cp̄ adequately describe p and its effects in the “real world” is not a question that can be answered by formal methods.

4. Correctness Proof: In the chosen framework, the programmer argues why the property ∀r(cp̄(r)) is true. Guided by some proof strategy, he reduces this proposition to other propositions whose correctness can be verified more easily. Ideally, the reasoning process is carried to an end where the propositions and the reasoning becomes so simple that it can be automatically checked by a computer. Practically, the reasoning process is stopped at a level where the correctness of the propositions is considered “obvious” for a human being.

2.2 Program Model and Implementation

The organization of program verification presented above contradicts the common view of the matter concerning the role of p and p̄, respectively:

• In the common view, p̄ is considered as the algorithm and the central point of discussion and p is considered as the implementation of p̄.

• In our view, p̄ is a model of p. Actually, we are interested in the properties of the program p and have introduced p̄′ to make the domain of discourse tractable.

The main difference between both points of view is the importance that is given to the “mapping” of p to p̄ or vice versa, respectively. Many promoters of the common view consider the design of p (if they are at all aware of the difference between p and p̄) as a tedious but actually not very interesting task (since p is just the implementation of the p̄ whose correctness has already been verified).

This view has its origin in the fact, that formal frameworks for sequential algorithms very well capture the main properties of real programs one is usually interested in. These properties are whether the program terminates and delivers the correct result for any valid input (and how long the computation takes). For an adequate description of these properties, many details of the program may be neglected. Most important, the model needs not contain any notion of time relations, since a program run can be easily modelled as a static sequence of variable assignments.

However, in parallel programming the gap between an abstract model and a concrete implementation is often very wide; a lot of textbooks on parallel algorithms use a notation that is far away from the constructs in which parallel programs have to be actually implemented. Many properties of the concrete program p can then not at all be derived from properties of the the abstract model p̄, since these properties essentially depend on aspects that are usually decided at the time of the implementation only. If we only construct an abstract model p̄ and verify its correctness, it is easily possible that the model will be to simple to capture the essentials of the concrete p.

Of course, before a programmer starts implementing a parallel program, he has designed some abstract algorithm p̄ and convinced himself about the correctness of the ideas expressed in p̄. However, as explained above, the actual implementation p will usually have a significant feedback also on p̄ making the model more realistic and useful. Therefore we think that a prototype implementation p should precede a formal verification of p̄. This has also the advantage that by testing p, many “trivial” errors in p̄ (like wrong boundary conditions) can be found in an early stage far more easily than by a formal verification.

2.3 The Complexity of Verification

But if p̄ is only a simplified model of p, are we then at least able to guarantee the correctness of p̄ within the formal framework? Before we discuss the question, we would like to draw attention to the issue of the complexity of program verification.

Verifications of sequential programs are compositional in the sense that properties of independent program parts can be independently verified. For instance, in order to prove

{a}P; Q{b}

in Hoare’s calculus, it suffices to prove for some proposition c

{a}P {c} ∧ {c}Q{b}

where both proofs can be carried through independently of each other. The verification of a large program can therefore be neatly decomposed into verifications of independent modules; the complexity of the verification reflects the complexity of the program structure.

In the case of parallel programs, the situation is fundamentally different. The proof of

{a}P ∥Q{b}

can not be decomposed into independent proofs on P and Q, since each operation in P may in general have some effect on the execution of Q. Instead, we have to show that if a initially holds, b holds after the execution of the program for any possible interleaving order of the program operations.

Of course, if the processes contain sequential modules that do not interact with other processes, these modules may be considered as “atomic” and their correctness can be independently checked by sequential verification methods. However, the complexity of the proof grows in a combinatorial way with the number of interactions and the number of processes involved in these interactions. Therefore, for tightly coupled parallel processes with complex interaction patterns a fully formal verification is in general not feasible. We consider this as a principal limit to formal program verification that can not be overcome no matter which formal framework is applied.

There are two possibilities to cut down the complexity of the verification to a tractable order. The first one is to use parallel programming languages that restrict the interaction between parallel processes to particular patterns for which simple formal frameworks can be constructed (see Subsection 2.5). Even if the parallel program is developed in a language that allows very general forms of interactions, many simplifications can be performed, if these general forms are not really applied. However, then the verification also has to include the proof that the simplifications are really valid, which may be a very complex task in its own.

For parallel programs where the general forms of interaction are actually applied, the only chance to make a verification manageable is to let the human brain serve as a “preprocessor” performing radical simplifications by investigating only the “interesting” cases and by combining several inference steps into one using “higher-order” verification rules. However, the justification of these simplifications itself is then necessarily an informal one and prone to human errors. The persuasion of the proof decreases up to some point where the verification itself becomes less convincing than the fact that the program p has shown the correct behavior for a finite amount of times.

The saying “testing is only able to detect errors, the absence of errors can be only guaranteed by a formal verification” seems therefore questionable. Verifications are not just “right” or “wrong” (this could be only checked by a computer if the verification was fully formal), they are more or less “convincing” for human beings! The whole process of parallel program verification is a steady tradeoff between the two extremes of simplicity and significance, between readable proofs that are not very persuasive and convincing proofs whose details nobody is able to follow.

These arguments are of course also true for the verification of sequential programs or (to some extent) for the proof of any mathematical properties. However, in the case of parallel program verification they become especially striking, since the principal complexity of the verification process itself is much larger.

2.4 The Purpose of Verification

What is then the use of parallel program verification? A fully formal verification is in general not tractable, it is uncertain whether the program model captures all important effects and the proof itself may contain large informal inference steps. A formal program verifications is therefore at least as prone to errors as the process of programming itself.

Actually we consider as the main value of the verification of a parallel program not the aspect of proving (in the sense of establishing without doubt) the correctness of a program but the aspect of documenting the programmer’s knowledge by 1. formal propositions that he believes to capture the essential properties of the program

and by

2. (semi-)formal arguments that support the believe in the correctness of these propositions.

By a program verification, the programmer is (by some proof strategy) forced to methodologically think about the program and to formulate his thoughts, his knowledge and his opinions as formal propositions and (semi-)formal proofs. By this process itself, many errors can be captured and the confidence in the correct behavior of a program can be considerably increased. The result of this process, the propositions and the proof, may then serve as a documentation of the program and as a trace of the programmer’s thoughts. Moreover, by the formal notation, the propositions can be irrefutably falsified by anybody that is able to construct counterexamples.

2.5 The Role of the Parallel Programming Model

The parallel programming model (respectively language) for implementing p may have some important impact on the verification process. The arguments concerning the complexity of parallel program verification presented in the previous subsections mainly applied to the classical parallel programming models with sequential processes coupled by a global store (shared memory programming) or special communication channels (message passing programming). The more tightly coupled the parallel processes are, the more complex their interaction and therefore their verification becomes.

On the other hand, parallel models based on concepts such as functional programming are much more easy to understand. The only interaction between processes occurs at the time of process creation (when arguments are passed) and process termination (when the result is delivered). For such models, no special parallel verification techniques are required, since here the correctness of the parallel program is a direct consequence of the correctness of the sequential program.

The parallel programming model of Paclib [HSN^{+}92] is a compromise between both extremes. If only the deterministic construct pacWaitOne is applied for communication between processes, the correctness of a Paclib program directly follows from the correctness of the corresponding Saclib program where all pacStart and pacWaitOne constructs are removed. Even if the non-deterministic pacWait construct is used, program verification is fairly easy. Only, if processes are coupled by streams using pacPut and pacGet (or even worse by buffers using pacRead and pacWrite), the verification of programs becomes extremely complex. The purely functional model of parallelism should therefore be preferred, since the resulting programs are by orders of magnitude far more easy to understand and to verify.

3 The PACLIB Kernel

The Paclib kernel is a runtime system for shared-memory multiprocessors that can be linked to any C program and provides light-weight concurrency together with a garbagecollected heap.

In this section, we will describe one aspect of the Paclib kernel whose correctness we are especially interested in: the non-deterministic task delivery scheme of the Paclib synchronization construct pacWait. The contents of this section are essentially taken from [Sch92].

3.1 The Programming Model

The Paclib model of parallelism is basically a functional one: A Paclib task receives certain Saclib objects as input arguments and returns a Saclib object as its result. This result may be retrieved later by a handle to this task.

     task = pacStart(fun, args)

creates a new task that executes fun(args) and can be referenced via the handle task. task is a first-order Saclib object i.e. it can passed to other functions or tasks or stored in a Saclib object. The result of this task (which is the value returned by fun) may be retrieved (arbitrarily often) by any task that knows task.

value = pacWait(tptr, tasks)

returns the result value of one of the tasks and writes the handle of the delivering task into the location tptr. If all denoted tasks are still active, pacWait blocks until one task terminates and then delivers the result of this task.

3.2 Task Creation

There are two separate entities defining a task:

• a task descriptor that exists as long as the task is alive.

• a result descriptor that exists as long as the task can be referenced.

The reason for this distinction is that the task descriptor is very large but only required as long as the task is running (i.e. its space can be reclaimed on the termination of a task). On the other hand, the result descriptor can be very small but it must exist as long as any other task might want to receive the task result.

The internal interpretation of the task handle returned by pacStart is that of a result descriptor which is a (reference to a) Saclib list with the following elements:

                              sem   task   wait   value

• sem is (a pointer to) a semaphore that provides mutual exclusion on the result descriptor.

• task is a pointer to the task descriptor of the task that computes the result. If the task has already delivered its result, task is the special constant AVAILABLE.

• wait contains, if task ≠ AVAILABLE, the head of the queue of task descriptors of all tasks blocked on an attempt to receive the result.

• value contains, if task ≠ AVAILABLE, the tail of the wait queue. If task = AVAILABLE, it contains the result of the task.

A task descriptor is a record that contains the workspace (i.e. the stack) of the task and the following fields (among others):

sem prev   next

result value wait sub stack   stop

• sem is a (pointer to a) semaphore that provides mutual exclusion on the task descriptor.

• prev and next connect all existing task descriptors into a doubly linked list.

• result is a reference to the result descriptor of the task.

• value is a location that receives the result of another task if the current task is blocked in a call of pacWait.

• wait contains, if the task is blocked in a call of pacWait, a list of those result descriptors that the current task is waiting for.

• sub is a list of result descriptors of all subtasks created by the current task.

• stack is an integer that denotes the stack size to be allocated for all tasks created by the current task.

• stop is a flag that is set if another task wants to abort the current task.

When a new task is started, a result descriptor and a task descriptor are allocated. The result descriptor is initialized with a new semaphore, a pointer to the task descriptor and an empty task queue. The fields of the task descriptor are initialized with the start address of the function to be executed, the corresponding arguments, a reference to the result descriptor and all the other values required to determine the task. The task descriptor is finally put into the ready queue for execution.

Actually, the new task does not execute the function fun provided by the user but a function pacShell that receives the address of fun and the corresponding arguments. pacShell calls fun and gets the result of this function call. This result is stored in the value field of the result descriptor and all tasks blocked on this descriptor are awaked. The task descriptor is then deallocated and the task terminates. The delivery of task results is described in the next subsection in more detail.

3.3 Task Results

The algorithm that implements pacWait works roughly as follows (the numbers in Figure 1 refer to the steps of the algorithm):

1. Lock: The semaphore associated to the descriptor t of the current task is locked. This prevents the tasks from delivering their result to t before pacWait has reestablished a consistent state.

2. Scan: All result descriptors in tasks are scanned and the result descriptor r of the current task is linked into the waiting queues of these descriptors.

3. Found: If a result descriptor in tasks already contains a result, r is removed from all waiting queues it has previously been linked into. t is unlocked and the result value is returned.

4. Sleep: If none of the results is already available, the result descriptor list tasks is stored in the wait field of t. t is unlocked and the current task is blocked.

5. Awake: After the task has been awaked, the value field of t contains the result of one of the tasks it waited for. Likewise, the wait field now contains the result descriptor of the task that returned the result.

After the pacShell has received the result of fun, it forwards the value to all tasks waiting on the result descriptor r (see Figure 2):

[figure: tasks; current task; wait; task_{1}; task_{2}; 1; 2/3; 4; 5]

Figure 1: Waiting for a Result

[figure: blocked task; wait; 1; 4; current task; rival task; 2; 3]

Figure 2: Delivering the Result 1. Pick Task: The semaphore associated to r is locked and the first task t waiting in the

queue is determined. In order to prevent a deadlock situation, r is unlocked before t is locked and then locked again. Without this detour, a rival task delivering its result to t might already have locked t and itself try to lock r in order to remove t from the waiting queue of r.

2. Check Task: If t has disappeared from the waiting queue of r, the corresponding task has in the meantime received its result from a slightly faster rival task. Otherwise, the current task has “won” the race and may deliver its result to t.

3. Remove Descriptor: t is removed from the waiting queue of r and from the waiting queues of all other result descriptors that the task is waiting for (the wait field of t holds a list of these descriptors). This guarantees that only one result is delivered to t.

4. Deliver Result: The result value is written into the value field of t and r is written into the wait field of t. The corresponding task is then awaked and can extract the desired information from t.

After the result has been delivered to all waiting tasks, it is written into the value field of r. The task field of r is set to AVAILABLE and r is unlocked. The task then unlinks the task descriptor from the global task list, releases its workspace and terminates.

3.4 Implementation

Appendix A shows the fraction of the source code of the Paclib kernel that implements the result delivery scheme described above:

• pacShell is the function that is executed by any Paclib task. It runs the denoted user function with the corresponding arguments and then calls pacResult.

• pacResult delivers the result to all blocked tasks and finally stores the value into the result descriptor. The function uses several macros that perform the basic functions on result descriptors (e.g. resLock) and task descriptors (e.g. taskLock). The function uWakeTask awakes a blocked task.

• pacWaitList is the basic function on which pacWait is based on. All task handles (i.e. result descriptors) are linked into a single list rlist. The function uBlockTask blocks the execution of the current task.

Attention: The source code given in the appendix is a slightly beautified, condensed and restructured version of the actual source code. The actual implementation is a bit more fault-tolerant, more optimized and more general than the functions shown there. However, the explanation of these details goes beyond the scope of the paper and we consider them of minor importance for our goal. The code given in the appendix would basically run as well. However, please note that already at this level of discussion we have performed some simplifications.

3.5 Verification Goal

Our goal is to formally justify our confidence in the correctness of the implementation of the Paclib result delivery scheme that has been presented in an informal way in this section and as a program in the appendix. We would like to verify that this non-deterministic scheme is correct for any program that applies pacStart and pacWait under all circumstances (i.e. possible interleavings of operations).

4 Temporal Logic and the Semantics of Programs

The formal framework we will use for reasoning is that of temporal logic as described in [Krö87]. The main reasons for this choice are the following:

• Axiomatic Approach: Temporal logic is an axiomatic approach to the formal treatment of parallel programs. It does not reason about the semantics of a program but about its properties. This is of particular importance since we want to deal with a whole class of (incompletely specified) programs.

• Intuitive Reasoning: Temporal logic allows intuitive reasoning about programs since it just models our usual knowledge about time relationships. Details that are “obvious” for a human being can be skipped if it would be tedious to derive them from the basic axioms.

• Hoare’s Calculus: As a special case, we can incorporate Hoare’s calculus for the verification of sequential programs into the temporal logic framework. This allows to reason about sequential program parts in the common way.

This section gives the essential core of [Krö87]. However, we describe the material in a language that is more amenable to computer scientists. Moreover, in Subsection 4.6 we introduce some concepts that make the reasoning process more practicable.

4.1 Temporal Logic

The main idea of temporal logic is to incorporate the notion of time into the framework of first-order predicate logic. We define time to be an infinite, discrete and linearly ordered sequence of time points with a smallest element:

τ_{0} < τ_{1} < τ_{2} < τ_{3} < …

The state of a universe S at each moment τ is defined by a valuation function η_{τ} that maps time-dependent quantities to values. Furthermore, a valuation function ξ maps timeinvariant quantities to their denotations. We may thus define a temporal structure K = (S, ξ, η) and a valuation function K_{τ} that describes the semantics of a formula A at a given time point t. Please note that in general K_{τ} (A) ≠ K_{τ′}(A) for τ ≠ τ′.

We define the semantics of atomic formulas and of the logical connectives as follows:

K_{τ} (A) = S^{(ξ,η_{τ})} for every atomic formula A
K_{τ} (¬A) = t  iff K_{τ} (A) = f
K_{τ} (A ∧ B) = t iff K_{τ} (A) = t and K_{τ} (b) = t
K_{τ} (A ∨ B) = t iff K_{τ} (A) = t or K_{τ} (b) = t
K_{τ} (A → B) = t iff K_{τ} (A) = f or K_{τ} (b) = t
K_{τ} (A ↔ B) = t iff K_{τ} (A) = K_{τ} (B)

For reasoning about time, we additionally introduce the unary temporal operators □ (“always”) ◇ (“sometime”) and ^{◯} (“next time”) and extend the valuation function K_{τ} by

K_{τ} (□A) = t iff K_{τ′}(A) = t for every τ′ ≥ τ
K_{τ} (◇A) = t iff K_{τ′}(A) = t for some τ′ ≥ τ
K_{τ} (^{◯}A) = t iff K_{τ+1}(A) = t

In other words, for a fixed moment τ, □A is true, iff A will hold from τ on forever. The semantics of the other operators is then also immediately clear.

The quantifiers ∀ and ∃ are defined by

K_{τ} (∀x(A)) = t iff K′_{τ} (A) = t for every K′ = (S, ξ′, η′)
with ξ′(y) =^{S} ξ(y) for every y other than x
K_{τ} (∃x(A)) = t iff K′_{τ} (A) = t for some K′ = (S, ξ′, η′)
with ξ′(y) =^{S} ξ(y) for every y other than x

We we also introduce the binary temporal operators atnext, before and until by

K_{τ} (A atnext B) = t iff K_{τ′}(A) = f for every τ′ ≥ τ or
K_{τ} (A) = t for the smallest τ′ > τ with K′_{τ} (B) = t
K_{τ} (A before B) = t iff if K_{τ′} = t for some τ′ > τ
then K_{τ′′} = t for some τ′′ with τ′ > τ′′ > τ
K_{τ} (A until B) = t iff K_{τ′} = t for some τ′ > τ and
K_{τ′′} = t for every τ′′ with τ′ > τ′′ > τ

Similar to classical first-order predicate logic, may introduce the notion of validity into temporal logic.

Definition 1 (Validity) A formula A is called valid in a temporal structure K (K-valid) if K_{τ} (A) = t for every time τ. A is called valid if A is valid in every K.

Please note that the temporal notion of validity has one more “degree of freedom” than the classical notion: A is valid in the temporal sense only if it is true at every time point!

Similar to the transformation rules for logical connectives and quantifiers, there are many “temporal rules” like

¬□A  ↔ ◇¬A
◯(A → B) ↔ ^{◯}A → ^{◯}B
□(A → B) → □A → □B
□(A ∧ B)  → □A ∧ □B
◇(A ∨ B)  → ◇A ∨ ◇B
□A ∨ □B  → □(A ∨ B)
∀x(^{◯}A)  ↔ ^{◯}∀x(A)
∃x(^{◯}A)  ↔ ^{◯}∃x(A)
∀x(□A)  ↔ □∀x(A)
∃x(◇A)  ↔ ◇∃x(A)

      A before B ↔ (¬B) atnext (A ∨ B)

These rules are intuitively clear but can be easily derived from the definitions above e.g.

K_{τ} (¬□A) = t iff not K_{τ′}(A) = t for every τ′ ≥ τ
iff K_{u}(A) = f for some τ′ ≥ τ
iff K_{u}(¬A) = t for some τ′ ≥ τ
iff K_{τ} (◇¬A) = t

For a much more comprehensive list of temporal rules, see [Krö87].

4.2 Parallel Programs

A parallel program Π consists of a set processes Π_{1} … Π_{p} each of which is a sequential program composed from the basic “assignment” statement and the statement builders “sequence” (the ; operator), “conditional” (one and two branch if statement) and “iteration” (while loop). All statements operate on the same global set of “program variables”. For the synchronization of parallel programs, there is a special statement

await C then v := E where C is a boolean condition and E is an expression to be assigned to the variable v. The intuitive semantics of this construct is that v := E can be executed only if C is true. Otherwise the process Π_{i} executing the await statement is blocked until C becomes true.

A program has the form

initial R; cobegin Π_{1} ∥ … ∥ Π_{p} coend

where R is a first-order formula called the initialization condition that describes the initial state of the program. As an example, take the following program

initial n = 0 ∧ sem cobegin (α_{0}) while i > 0 do (α_{1}) await sem then sem := false (α_{2}) stack[n] := i (α_{2}) n := n + 1 (α_{3}) sem := true (α_{4}) i := i − 1

endwhile (α_{e}) stop ∥ (β_{0}) while j > 0 do (β_{1}) await sem then sem := false (β_{2}) stack[n] := j (β_{2}) n := n + 1 (β_{3}) sem := true (β_{4}) j := j − 1

endwhile (β_{e}) stop coend

where two processes concurrently push items on a stack. A boolean variable sem (a “semaphore”) is used for providing mutual exclusion of both processes during the stack access. Further on, we will use for semaphore operations the notation

P(sem) ≡ await sem then sem := false V(sem) ≡ sem := true

which is more common in parallel programming than the await construct. The stop statement in the program above is actually a shortcut for

stop ≡ await false

and always denotes the last statement in each parallel process beyond which execution cannot proceed. All statements in the program are labelled for a unique reference. The set of all labels in a program Π is denoted by M_{Π}; the set of all labels without the trailing stop labels is denoted by \overline{M}_{Π}.

4.3 Program Execution

The computational behavior of a parallel program is described by an interleaving model of execution where at each time point one atomic operation of a single process is executed.

Definition 2 (Atomic Operation) An atomic operation is

• an assignment statement, • an await statement (test of condition and execution of the assignment),

• a test of the condition in an if statement (and entry in the respective branch),

• a test of the condition in an while statement (and entry into or exit from loop). Definition 3 (Program State) The state of a program Π at a time point τ is a tuple

η_{τ} = (μ, λ_{1}, …, λ_{p}, κ) where

• μ(a) is the value of the program variable a at time τ,

• λ_{i} is the label of the statement of Π_{i} that is ready to be executed at time τ,

• κ ≠ 0 means that Π_{κ} is the process (and thus λ_{κ} is the statement) scheduled for execution at time τ,

• κ = 0 means that no Π_{i} may be scheduled at τ and therefore also not at any time

τ′ > τ (deadlock or terminal state). The possible transitions from one program state to another will be described by a set of tuples (λ, C, λ′) saying that, if the condition C is true, execution may proceed from statement λ to λ′. Definition 4 (Transitions) The set trans(Π) of possible transitions of a sequential program Π is inductively defined on the structure of Π :

1. Stop: If Π is the statement

λ_{l} : stop then trans(Π) = ∅.

2. Assignment: If Π is an assignment

\begin{matrix}λ_{l} : v := E \\ λ_{m} : … \end{matrix}

then trans(Π) = {(λ_{l}, t, λ_{m})}.

3. Wait Statement: If Π is a wait statement λ_{l} : await C then …

λ_{m} : …

then trans(Π) = {(λ_{l}, C, λ_{m})}.

4. Sequence: If Π is a sequence

\begin{matrix}λ_{l} : Π_{1} \\ λ_{m} : Π_{2} \\ λ_{n} : … \end{matrix}

then trans(Π) = trans(Π_{1}) ∪ trans(Π_{1}).

5. Two Branch Conditional: If Π is a two branch conditional λ_{l} : if C then λ_{m} : Π_{1} else λ_{n} : Π_{2} endif

λ_{o} : …

then trans(Π) = {(λ_{l}, C, λ_{m}), (λ_{l}, ¬C, λ_{m})} ∪ trans(Π_{1}) ∪ trans(Π_{2}).

6. One Branch Conditional: If Π is a one branch conditional λ_{l} : if C then λ_{m} : Π_{1} endif

λ_{n} : …

then trans(Π) = {(λ_{l}, C, λ_{m}), (λ_{l}, ¬C, λ_{n})} ∪ trans(Π_{1}).

7. While Loop If Π is a while loop

λ_{l} : while C do λ_{m} : Π_{1} endwhile
λ_{n} : …

then trans(Π) = {(λ_{l}, C, λ_{m}), (λ_{l}, ¬C, λ_{n})} ∪ trans(Π_{1}).

In this informal definition, the trailing statement “…” denotes the successor of the current statement (such a successor exists and is unique for all statements but the final stop statement in a process). The exact definition of trans(Π) can be found in [Krö87].

Definition 5 (Statement Execution) For every α ∈ M_{Π}, we define the execution condition

E_{α} = \{ \begin{matrix}C, & if α : await C then v :=E \\ true, & otherwise \end{matrix}

We may now define the structure of valid execution sequences of a program.

Definition 6 (Execution Sequence) An execution sequence of Π is an infinite sequence η = (η_{0}, η_{1}, η_{2}, …) of program states such that

1. Initial State: η_{0} = (μ, α_{0}^{1}, …, α_{0}^{p}, κ) and K_{0}(R) = t.

2. Transition: If η_{τ} = (μ, λ_{1} … λ_{κ} … λ_{p}, κ > 0) then η_{t+1} = (μ′, λ_{1} … λ′_{κ} … λ_{p}, κ′) and, for some formula C, (λ_{κ}, C, λ′_{κ}) ∈ trans(Π_{κ}) and K_{τ} (C) = t.

3. Terminal State: If η_{τ} = (μ, λ_{1}, …, λ_{p}, 0) then η_{τ+1} = η_{τ} and K_{τ} (E_{λ_{i}}) = f for every 1 ≤ i ≤ p.

Please note that this definition does not give the semantics of the assignment and await statement since it does not describe the relationship between μ and μ′ on a state transition.

4.4 Temporal Program Semantics

The language of temporal logic described in Subsection 4.1 is not yet sufficient to describe program states since it does not give any possibility to express information about the program counters λ_{1}, …, λ_{p}, κ in a program. For this purpose, we introduce the following set of propositional variables:

1. at{λ} for every λ ∈ M_{Π}.

2. λ for every λ ∈ \overline{M}_{Π}.

The informal meaning of the proposition at{λ} is “the statement λ is ready for execution in some process Π_{i}” while λ means “the statement λ is executed next”. The information expressed by the program state

η_{τ} = (μ, λ_{1}, …, λ_{p}, κ)

with κ > 0 can then be expressed by the formula

(v_{1} = μ(v_{1})) ∧ … ∧ (v_{n} = μ(v_{n})) ∧ at{λ_{1}} ∧ … ∧ at{λ_{p}} ∧ λ_{κ}

where the v_{i} are the program variables occurring in Π.

In the notion of temporal logic, we may therefore interpret a program state η_{τ} as a valuation function

η_{τ} (v) = μ(v)  for every program variable v
η_{τ} (λ) = t  iff λ = λ_{κ} and κ ≠ 0
η_{τ} ( at{λ}) = t iff λ = λ_{j} for some j

We may now apply the notion of validity defined in Subsection 4.1 to the special case of execution sequences.

Definition 7 (Π-Validity) A formula A is Π-valid if it is true for every execution sequence η of Π (at any time τ).

However, the restriction of temporal structures to execution sequences of programs can be also described by giving additional axioms and rules for deriving more formulas. We will distinguish between two kinds of axioms

1. Structural Axioms that are invariant for any program Π,

2. Computation Scheme Axioms that depend on Π.

It can be proved that a formula is Π-valid if it can be derived using these axioms [Krö87] where the following abbreviation is used:

Definition 8 (Initial and Terminal State) For any process Π with M_{Π} = {α_{0}, …, α_{l}} we define

start_{Π} ≡ at{α_{0}^{i}} ∧ … ∧ at{α_{0}^{p}} ∧ R
nil_{Π}  ≡ ¬α_{1} ∧ ¬α_{2} ∧ … ¬α_{l}

The informal meaning of start_{Π} is “Execution of Π is in its initial state” while nil_{Π} says “No statement is executed in Π”. The structural axioms are then the following:

Rule 1 (Basic Rule) A is always true if it holds permanently beginning with the initial state of the execution sequence:

start_{Π} → □A ⊢ A.

Axiom 1 (Basic Axiom) If no statement is executed, nothing changes:

nil_{Π} ∧ A → ^{◯}(nil_{Π} ∧ A).

Axiom 2 (Two Execute) No two statements execute at the same time:

∀λ ≠ λ′(λ → ¬λ′).

Axiom 3 (Execute) An statement may only execute if it is ready to:

∀λ(λ → at{λ}).

Axiom 4 (Two Ready) In every Π_{k}, no two statements are ready to execute at the same time:

∀k, l, m( at{λ_{l}^{k}} ∧ l ≠ m → ¬ at{λ_{m}^{k}}).

Axiom 5 (Enabled) If some statement is enabled, then some statement has to execute:

∀λ( at{λ} ∧ E_{λ} → ¬nil_{Π}).

Axiom 6 (Ready) An statement ready to execute but not executing remains ready:

∀λ( at{λ} ∧ ¬λ → ^{◯} at{λ}).

Axiom 7 (End) If Π_{i} has reached its end label then it remains there:

∀k( at{λ}_{e}^{k} → ^{◯} at{λ}_{e}^{k}).

Axiom 8 (Change) Every non-assignment and non-wait statement does not cause any variable changes:

∀λ ∉ {:=, await} ∀P ∉ LP(λ ∧ P → ^{◯}P).

The set of axioms describing the behavior of a particular program Π can be derived from the following axiom:

Axiom 9 (Computation Scheme) For every λ ∈ M_{Π}, the following holds

λ → (C_{1} ∧^{◯} at{λ_{1}}) ∨ … ∨ (C_{q} ∧^{◯} at{λ_{q}}).

where (λ, C_{1}, λ_{1}), …, (λ, C_{q}, λ_{q}) are all transitions with first statement λ in trans(Π).

Actually, this axiom is more general than necessary and can (according to the definition of trans(Π)) be replaced by the following set of axioms that are more intuitive:

Axiom 10 (Assignment Statement) If λ_{l} is an assignment statement i.e.

λ_{l} : v := E
λ_{m} : …

then execution proceeds from λ_{l} to λ_{m}:

λ_{l} → ^{◯} at{λ_{m}}.

Axiom 11 (Wait Statement) If λ_{l} is a wait statement i.e.

λ_{l} : await C then …
λ_{m} : …

then the condition C lets execution either suspend or proceed from λ_{l} to λ_{m}:

λ_{l} → (C → ^{◯} at{λ_{m}}) ∧ (¬C → ^{◯} at{λ_{l}}).

Axiom 12 (Two Branch Conditional) If λ_{l} is the label of a two branch conditional i.e.

λ_{l} : if C then λ_{m} : … else λ_{n} : … endif

then the condition C lets execution proceed from λ_{l} to one of the branches λ_{m} or λ_{n}, respectively:

λ_{l} → (C → ^{◯} at{λ_{m}}) ∧ (¬C → ^{◯} at{λ_{n}}).

Axiom 13 (One Branch Conditional) If λ_{l} is the label of a one branch conditional i.e.

λ_{l} : if C then λ_{m} : … endif
λ_{n} : …

then the condition C lets execution proceed from λ_{l} either to the branch λ_{m} or to the successor λ_{n}:

λ_{l} → (C → ^{◯} at{λ_{m}}) ∧ (¬C → ^{◯} at{λ_{n}}).

Axiom 14 (While Loop) If λ_{l} is the label of a while loop i.e.

λ_{l} : while C do λ_{m} : … endwhile
λ_{n} : …

then the condition C lets execution either proceed to the next iteration of the body λ_{m} or to the successor λ_{n}:

λ_{l} → (C → ^{◯} at{λ_{m}}) ∧ (¬C → ^{◯} at{λ_{l}}).

The effect of the assignment and the await statement is described by the following

Axiom 15 (Assignment) For every statement

λ : v := E

and every statement

     λ : await C then v := E

the following holds for every non-temporal formula P:

λ ∧ P_{v}(E) → ^{◯}P.

The whole set of axioms describing the properties of a program Π is also called the temporal semantics of Π.

4.5 Description of Program Properties

There are basically two kinds of program properties that are of interest:

1. Safety (or Invariance) Properties,

2. Liveness (or Eventuality) Properties.

Invariance properties are expressed by formulas of the form

A → □B.

For instance, the partial correctness of a program with precondition P and postcondition Q can be expressed by the formula

start_{Π} ∧ P → □(( at{α_{e}^{1}} ∧ … ∧ at{α_{e}^{p}}) → Q)

saying that if Π starts with P then Q always holds in the terminal state.

Eventuality properties are expressed by formulas of the form

A → ◇B.

As an example take the termination of a program with precondition P that can be written

start_{Π} ∧ P → ◇( at{α_{e}^{1}} ∧ … ∧ at{α_{e}^{p}})

saying that if Π starts with P then it will eventually reach the terminal state.

The proof of invariant properties can be based on the following rule

Rule 2 (Invariant) In order to prove “if A now holds then B always holds from now on”, it suffices to prove that B follows from A and that B is invariant under every statement:

(A → B) ∧ ∀λ ∈ \overline{M}_{Π} (λ ∧ B → ^{◯}B) ⊢ A → □B.

For proving eventuality properties, we are faced with the problem that some “natural” program properties can not be derived from the set of axioms specified up to now. Consider e.g. the program

initial a = 1 cobegin (α_{0}) a := 0 (α_{e}) stop ∥ (β_{0}) while a = 1 do (β_{1}) b := 0

endwhile (β_{e}) stop coend

Clearly we would claim that in any reasonable model of parallel execution Π should terminate sometime i.e. α_{e} should be reached. In other words,

start_{Π} → ◇ at{α_{e}}

should be Π-valid but unfortunately it is not. The reason for this is that there is one execution sequence in which above formula is not true, namely that where forever β_{0} and β_{1} are alternately scheduled for execution. In order to overcome this deficiency, we introduce the notion of “fairness”:

Definition 9 (Fairness) An execution sequence η = (η_{0}, η_{1}, η_{2}, …) of a program Π is called fair it has the following property: If there are infinitely many states

η_{τ} = (μ, λ_{1}, …, λ_{i}, …, λ_{p}, κ)

containing the same λ_{i} such that K_{τ} (E_{λ_{i}}) = t, then κ = i in infinitely many η_{τ}.

From now on, a formula A is considered Π-valid if it is valid in every fair execution sequence. Equivalently, this restriction can be described by the following

Axiom 16 (Fairness) If an statement is enabled infinitely often then it will be executed sometime:

∀λ((□◇( at{λ} ∧ E_{λ})) → ◇λ).

This notion of fairness is also compatible with all process schedulers that apply a round-robin strategy with preemptive execution of processes (like the Paclib scheduler).

Definition 10 (Process Execution) For any process Π_{i} with \overline{M}_{Π_{i}} = \{α_{0}^{i}, …, α_{m}^{i}\} we define the execution condition E^{i} as

E^{i} ≡ ( at{α_{0}^{i}} ∧ E_{α_{0}^{i}}) ∨ … ∨ ( at{α_{0}^{e}} ∧ E_{α_{0}^{e}})

The informal meaning of E^{i} is “one of the statements in Π^{i} is enabled for execution”. This predicate is used in the following rule on which the proof of eventually properties is based.

Rule 3 (Well Founded Orderings) To prove that B will eventually hold it suffices to prove that there is a well-founded ordering (Z, ⪯) and a term z such that no statement in Π increases z with respect to this ordering, that there is for each value of z a ““helpful” process Π_{h(z)} decreasing z and that Π_{h(z)} will be eventually scheduled for execution:

α ∧ A(z) → ^{◯}(B ∨ ∃z′(z′ ⪯ z ∧ A(z′))) for every α ∈ \overline{M}_{Π}\\overline{M}_{Π_{h(z)}},
α ∧ A(z) → ^{◯}(B ∨ ∃z′(z′ ≺ z ∧ A(z′))) for every α ∈ \overline{M}_{Π_{h(z)}}
□A(z) → ◇(B ∨ E^{Π_{h(z)}})
⊢ ∃z(A(z)) → ◇B

4.6 Time Constants

The standard framework of temporal logic does not give any possibility for explicitly referencing time points. [Krö87] says

Consider now a proposition A. In order to describe the possible variety of the truth values of A at different times t the simplest linguistic means would be to introduce an explicit time parameter in the proposition and and denote it by A(t). The main idea of the logical language we want to define, however, is to avoid just such an explicit occurrence of time. The reason is that we do not really want to be able to express assertions like “A is true at t_{17}”. We rather want to have at hand logical operators which enable us to formulate new propositions about the truth values of A at time points which are related to some reference point (the present time) in particular ways.

We agree with the statement that we are not interested in expressing assertions like “A holds at t_{17}”. However, we argue that time references are nevertheless useful for using

1. different “reference systems” in formulas,

2. a more general induction rule for proving.

The first item addresses the fact that even within a fixed temporal structure K the assertion

A

has not a unique meaning since it does not say when A holds. By just writing down A, it is not clear whether we want to say K_{17}(A) = t or K_{23}(A) = t or K_{τ} (A) = t where τ is the “present time”. The usual solution is to consider A as a shortcut for

□A.

However, the definition of the □ operator

K_{τ} (□A) = t if K_{τ′}(□A) = t for every τ′ > τ

shows that we have shifted the problem only to another level. The denotation of □A still depends on the reference point τ considered as the “present time”. In program verification, the usual attitude is to consider the the start time of a program as the reference time 0 and to express all assertions relative to this time. Therefore, A is actually a shortcut for

K_{0}(□A) = t.

If we want to reference another time point τ_{A} during a program run, we therefore have to find a unique characterization by a condition A on the state of the program variables and of the location counters such that

K_{τ_{A}}(A) = t and K_{τ} (A) = f for every τ ≠ τ_{A}.

The assertion “B holds at τ_{A}” is then expressed by A → B. However, this indirect way of referencing time points makes propositions often difficult to understand. We have to remember that the formula is a shortcut for K_{0}(□(A → B)) = t which can be reduced to

K_{τ_{A}}(B) = t.

what we actually would like to say. The problem is that the one-to-one correspondence between A and τ_{A} is not a priori clear from the formula. This is especially annoying if we want to switch to another reference time i.e. to formulate a set of formulas relatively to some τ_{A}. We therefore propose to directly reference particular time points by the introduction of time constants.

Definition 11 (Time Constants) For every time τ there is a constant τ defined by

\begin{aligned}K_{τ′}(τ) & = t & if τ = τ′ \\ & = f & if τ ≠ τ′ \end{aligned}

A formula τ → A is therefore a shortcut for K_{0}(□(τ → A)) which can be reduced to

K_{0}(□(τ → A)) = t if K_{τ′}(τ → A) = t for every τ′ ≥ 0
if K_{τ} (A) = t

i.e. the interpretation of the formula is directly clear from its syntactic structure. In a similar way, the interpretation of τ_{0} → (A until τ_{1}) can be reduced to

K_{0}(□(τ_{0} → (A until τ_{1}))) = t if K_{τ} (A) = t for every τ with τ_{0} ≤ τ < τ_{1}

which is immediately clear from the formula itself.

The purpose of time constants is therefore to constrain the reference time (respectively the time range) of a formula and to make this constraint explicit in the formula. We will therefore say that τ is the reference time of A in a context τ → A and that the interval [τ_{0} … τ_{1}[ is the time range of A in a context τ_{0} → (A until τ_{1}). We will in our verification only use such constrained formulas.

Furthermore, we introduce an additional structural program axiom that defines a special time constant for the start time of a program Π:

Axiom 17 (Start) τ_{Π} is the start time of the program Π:

τ_{Π} → start_{Π}.

This implies that in the context of program verification for each time τ the assertion τ > τ_{Π} holds. By Axiom 8 (Initial State), we then know

τ_{Π} → □A ⊢ A

The definition of a new time constant τ will always depend on previously defined time constants starting with τ_{Π}. This definition will be based on a characteristic condition A (as explained above) e.g. by saying

     τ_{Π} → τ atnext A

(where we have to prove that τ_{Π} → ◇A). After this definition, we may therefore use the symbol τ to reference the denoted time and apply the assertion τ → A.

A second advantage of introducing time constants is the possibility of applying a generalized induction rule. A proof guided by Rule 2 (Invariant) only allows conclusions from one statement to the next. We think that this view does not reflect the way most human beings intuitively reason about a program. Consider e.g. the program

initial n = 0 ∧ N ≥ 0 ∧ sem cobegin Π_{1} ∥ … ∥ Π_{p} coend

where each Π_{i} is constructed as follows:

(α_{0}^{i}) P(sem)
(α_{1}^{i}) while n < N do
(α_{2}^{i}) s_{i} := n
(α_{3}^{i}) n := n + 1
(α_{4}^{i}) V(sem)
(α_{5}^{i}) a[s_{i}] := s_{i}
(α_{6}^{i}) P(sem)

endwhile (α_{7}^{i}) V(sem)

(α_{e}^{i}) stop

Suppose that we want to verify

□(∀i( at{α_{e}^{i}}) → ∀j < N(a[j] = j)). (1)

i.e. that at the termination of the program a[j] = j holds for every j.

Proof: For proving this assertion we describe the temporal behavior of the program by the formula

A ≡
(n ≤ N,
sem → (B_{n} ∧ ∀i(C_{i})),
¬sem → ∃k(C_{k} ∧ ∀i ≠ k(¬C_{k})),
∀i( at{α_{1}^{i}} → ¬sem ∧ B_{n}),
∀i( at{α_{2}^{i}} → ¬sem ∧ B_{n} ∧ n < N ∧ E),
∀i( at{α_{3}^{i}} → ¬sem ∧ B_{n} ∧ n < N ∧ s_{i} = n ∧ E),
∀i( at{α_{4}^{i}} → ¬sem ∧ B_{n−1} ∧ n ≤ N ∧ s_{i} = n − 1 ∧ E),
∀i( at{α_{5}^{i}} → s_{i} < n),
∀i( at{α_{7}^{i}} → ¬sem ∧ n = N ∧ B_{n}),
∀i( at{α_{e}^{i}} → n = N ∧ B_{n})).

where B_{n}, C_{i} and D are defined as

B_{n} ≡ ∀j < n(a[j] ≠ j → ∃k( at{α_{5}^{k}} ∧ s_{k} = j)), (2) C_{i} ≡ at{α_{1}^{i}, …, α_{4}^{i}, α_{7}^{i}}, (3) D ≡ ∀k(¬ at{α_{e}^{k}}). (4)

The truth of (1) is a direct consequence of □A.

For proving □A, we have to prove by Rule 2 (Invariant) start_{Π} → A (which is easy) and, for each λ, λ ∧ A → ^{◯}A. We will only show the case λ = α_{4}^{i} (for some i):

1. α_{4}^{i} and n ≤ N imply ^{◯}n ≤ N.

2. α_{4}^{i} and A imply ¬sem, B_{n−1} and s_{i} = n−1. A and ¬sem imply ∃k(C_{k} ∧∀i ≠ k(¬C_{k})); α_{4}^{i} implies C_{i} and ^{◯}¬C_{i} and therefore ^{◯}∀i(¬C_{i}). B_{n−1}, s_{i} = n − 1 and ^{◯} at{α_{5}^{i}} imply ^{◯}B_{n}.

3. α_{4}^{i} implies ^{◯}sem.

4. ^{◯}∀i(¬C_{i}) and ¬E imply ^{◯}¬ at{α_{1}^{i′}, …, α_{4}^{i′}, α_{7}^{i′}, α_{e}^{i′}} for all i′. ^{◯} at{α_{5}^{i′}} implies at{α_{5}^{i′}}, therefore s_{i′} < n and thus ^{◯}s_{i′} < n. □

Please note that have only shown one of eight cases (for each α_{l}^{i} in the program)! A full verification of even this toy program becomes therefore very complex. This “statementoriented” view is therefore not feasible for the verification of “real” parallel programs since the overview on the main lines of the proof easily goes lost. However, by the introduction of explicit time references we can use the following generalized induction rule that we think is more easier to use also for “semi-formal” proofs:

Rule 4 (Induction) In order to prove “if A holds at τ_{A} then B always holds from τ_{A} on”, it suffices to prove that B follows from A at τ_{A} and that B is true at every τ under the assumption that it has been true from τ_{A} until τ:

(τ_{A} → (A → B)) ∧ ∀τ > τ_{A}((τ_{A} → (B until τ)) → (τ → B)) ⊢
τ_{A} → (A → □B).

We will apply this rule to the program presented before. The main ideas there are

1. sem guarantees mutual exclusion on n,

2. B_{n} holds outside the critical region protected by sem,

3. n = N holds at the end of the program.

Proof: The mutual exclusion property

□((sem → ∀i(C_{i})) ∧ (¬sem → ∃i(C_{i} ∧ ∀k ≠ i(¬C_{k})))) (1)

is easy to verify since α_{0}^{i} and α_{6}^{i} are the only entries and α_{4}^{i} and α_{7}^{i} the only exits from the critical region. Now let us prove that

□(sem → B_{n}) (2)

By Rule 4 (Induction Rule), we have to prove τ_{Π} → B_{n} which is clear since τ_{Π} → n = 0. Now take an arbitrary fixed time τ > τ_{Π} and assume

(3) τ_{Π} → ((sem → B_{n}) until τ) , τ → sem . (4)

We have to prove τ → B_{n}. Let τ′ = τ − 1. We only have to consider those cases where the truth value of sem → B_{n} may become false i.e. where τ′ → ¬sem (at the exits of critical regions) or where indeed τ′ → sem (and thus by the induction hypothesis τ′ → B_{n}) but perhaps τ → ¬B_{n}. Actually, there are only the following cases are of interest:

1. τ′ → (α_{4}^{i} ∨ α_{7}^{i}): We know τ′ → ¬sem. Let τ′′ be the largest τ′′ < τ′ with τ′′ → sem. By the induction hypothesis, we then know τ′′ → B_{n}. By the program structure, we know τ′′ → (α_{0}^{i} ∨ α_{6}^{i}) and τ′′ → ^{◯}α_{1}^{i}. By (1), we know τ′′ → (s_{i} = n − 1 ∧ B_{n−1}) atnext α_{4}^{i} i.e. τ′ → (s_{i} = n − 1 ∧ B_{n−1}). We thus have τ → B_{n}.

2. τ′ → α_{5}^{i}: If τ′ → sem, we know by the induction hypothesis τ′ → B_{n}. We also know τ′ → at{α_{5}^{i}} and τ′ → ^{◯}¬ at{α_{5}^{i}} but also τ′ → ^{◯}a[s_{i}] = s_{i}. Thus τ′ → ^{◯}B_{n}.

If τ′ → ¬sem, let τ′′ be the largest τ′′ < τ′ with τ′′ → sem. By the induction hypothesis, we know τ′′ → B_{n}. Since τ′′ → ¬sem until τ′, it is by mutual exclusion and the program structure clear that, for any n̄, τ′′ → n = n̄ implies τ′ → n ≤ n̄ + 1 and therefore τ′ → B_{n−1}. This implies τ → B_{n} with the above argument.

The fact that

τ_{Π} → □∀i( at{α_{e}^{i}} → n = N) (5)

can be checked as follows. Let τ and i be arbitrary fixed such that

τ → at{α_{e}^{i}}. (6)

By the program structure, it is clear that τ → n ≥ N. Now assume τ → n > N. In this case, there exists some τ′ < τ and some i′ such that

τ′ → (n = N ∧ α_{3}^{i′}). (7)

By (1), this implies that for the largest τ′′ < τ′ with τ′′ → α_{2}^{i′} we have τ′′ → n = N and therefore τ′′ → ^{◯} at{α_{7}^{i′}} which contradicts (7). □

The application of Rule 4 (Induction) does of course principally not save any work; the complexity of a formal proof is as large as a proof carried through by Rule 2 (Invariant) (since in the induction step a case distinction over all statements is required). The main advantage of this new rule is that it allows to “jump back” in one step to a past time-point where something “interesting” has happened (e.g. to the entry of a critical region).

We may then apply the induction hypothesis to this time point and proceed to the “current” time point. The reasoning on the “uninteresting” intermediate points (e.g. within a critical region) may be then less formal. In the “statement-oriented” style of reasoning, such jumps are not possible. There the behavior of the program has to be described for each statement and verification has to proceed from one statement to the next.

For the use of Rule 4 (Induction), we introduce the “backward” oriented time operators △ (“previous time”) and atprev:

K_{τ} (△A) = t  iff  K_{τ−1}(A) = t and τ > 0
K_{τ} (A atprev B) = t iff  K_{τ′}(A) = t for some τ′ < τ
and K_{τ′}(B) = t for the largest τ′ < τ
with K_{τ′}(A) = t

Statements like “Let τ′ = τ − 1; we know τ′ → A” can now by replaced by τ → △A.

For proving facts like τ_{s} → (B until τ_{e}) we will apply

Rule 5 (Bounded Induction) In order to prove “if A holds at τ_{s} then B always holds from τ_{s} up to τ_{e}”, it suffices to prove that B follows from A at τ_{s} and that B is at every τ true before τ_{e} under the assumption that it has been true from τ_{s} on up to τ:

(τ_{s} → (A → B)) ∧ ∀τ_{e} > τ > τ_{s}((τ_{s} → (B until τ)) → (τ → B)) ⊢
τ_{s} → (A → (B until τ_{e})).

This is a slight generalization of Rule 4 (Induction).

5 The Formal Model

5.1 The Overall Design

Our verification will be based on the following model program

Π ≡ init I ∧ J
cobegin Π_{1} ∥ … ∥ Π_{p} coend

where each process Π_{k} has the structure

…
(β_{1}^{k}) waitk(y_{k}, r_{k}, R_{k})
(β_{e}^{k}) nop
…
(α_{1}^{k}) resultk(x_{k})
(α_{e}^{k}) stop

Each process may contain an arbitrary number of wait calls (with arbitrary local computations between these calls) and is terminated by a result call. The informal meaning of these functions is

1. wait(y, r, R) waits for the result of one of the Π_{i} where i is in the set R. After returning from the call, r holds one of these identifiers and y holds the result of Π_{r}.

2. result(x) makes the process result x public to all processes that currently wait for this result or will at a later time point try to retrieve the result.

The nop (no operation) statement after the wait call only serves as a reference to the last instruction of wait, the stop statements after result terminates the program.

Please note that our model only describes the synchronization of Paclib programs by pacWait but not the creation of new processes by pacStart. However, we will never use the process number p in our verification; the proof also works for an infinite number of processes and therefore also for programs that create new processes at runtime.

Furthermore, we do not demand that all the Π_{k} execute the same program. In fact, we do not at all make any assumptions about the structure of the processes before or after a particular wait call. Our verification will therefore be valid for any set of processes that use the wait construct.

Before we describe the initialization conditions I and J and the internal structure of wait and result, we will formulate the correctness theorem that we are going to verify.

5.2 The Correctness Theorem

The correctness of the program is established by the following theorem.

Theorem 1 (Correctness) For every process j that calls wait_{j}(y_{j}, r_{j}, R_{j}) the following holds:

1. No Result: If no process i in R_{j} has ever executed or will ever execute result_{i}, then j will not return from the wait_{j} call.

2. Some Result: If some process i in R_{j} has executed or will execute result_{i} then the following holds:

(a) Wait Continuation: j returns from the result_{j} call.

(b) Result Delivery: after returning from result_{j}, the variable r_{j} holds some identifier i of R_{j} and the variable y_{j} holds the corresponding result x_{i}.

Formally,

∀j ∀τ_{w} ≥ τ_{Π} ∀\overline{R} ∀\overline{x} (
(τ_{Π} → □∀i(α_{1}^{i} → x_{i} = \overline{x}_{i})) ∧ (τ_{w} → (β_{1}^{j} ∧ R_{j} = \overline{R}_{j})) →
(τ_{Π} → ∀i ∈ \overline{R}_{j}(□¬α_{1}^{i})) →
(τ_{w} → □¬β_{e}^{j}) ∧
(τ_{Π} → ∃i ∈ \overline{R}_{j}(◇α_{1}^{i})) →
(τ_{w} → ◇β_{e}^{j}) ∧
(τ_{w} → ((r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}) atnext β_{e}^{j}))).

We will now explain this correctness theorem in more detail. The theorem contains the following mathematical constants and statement labels:

• j is the identifier of a process waiting for the result.

• τ_{w} is the time when j performs the wait_{j} call.

• \overline{R}_{j} is the “wait set” of j in this wait_{j} call.

• \overline{x}_{i} is the result of Π_{i} (for all i).

• β_{1}^{j} is the label of the wait_{j} call.

• β_{e}^{j} is the label of the last statement of wait_{j}.

• α_{1}^{i} is the label of the result_{i} call of Π_{i} (for all i).

The theorem formulates an assertion for each process j that performs a wait_{j} call at some time point τ_{w} with some wait set \overline{R}_{j}.

The first assumption

τ_{Π} → □∀i(α_{1}^{i} → x_{i} = \overline{x}_{i})

declares the result of each process Π_{i} as the value of the program variable x_{i} at the time at which Π_{i} calls result_{i}. The result is associated to the mathematical constant \overline{x}_{i}, which is necessary because the value of x_{i} needs not be the same any more at the time when the wait_{j} call returns the result of Π_{i}.

The second assumption

τ_{w} → (β_{1}^{j} ∧ R_{j} = \overline{R}_{j})

defines τ_{w} to be the time at which Π_{j} calls wait_{j} and associates the contents of the program variable R_{j} to the mathematical constant \overline{R}_{j}. This is required since the value of R_{j} may be changed during the program run.

The theorem then describes two cases:

1. τΠ → ∀i ∈ \overline{R}j(□¬αi1)

is the case when no process i ∈ \overline{R}_{j} has ever called result_{i} (i.e. before wait_{j} is called) or will ever call result_{i} (i.e. after wait_{j} has been called). The reference time of the assumption is therefore the program start time τ_{Π} and the □ operator refers to the total runtime of the program. The conclusion

τ_{w} → □¬β_{e}^{j}

says that Π_{j} will never return from this particular wait_{j} call (but it does not say anything about former wait_{j} calls of Π_{j}). The reference time of the conclusion is therefore the time τ_{w} when wait_{j} is called and the □ operator only refers to the future of τ_{w} (but not to the time between τ_{Π} and τ_{w}).

2. τΠ → ∃i ∈ \overline{R}j(◇αi1)

is the case when some process i ∈ \overline{R}_{j} has terminated before τ_{w} or will terminate after τ_{w}. The reference time of the assumption is therefore τ_{Π} and the ◇ operator refers to the total runtime of the program. The first conclusion

τ_{w} → ◇β_{e}^{j}

says that Π_{j} will return from this particular wait_{j} call, i.e. it will execute β_{e}^{j} after τ_{w}. The second conclusion

τ_{w} → ((r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}) atnext β_{e}^{j})

says that after returning from this wait_{j} call r_{j} holds one of the process identifiers of \overline{R}_{j} and that y_{j} equals the result of this process. The reference time of this statement is therefore τ_{w}. It is not necessary to express by extra assertion that Π_{r_{j}} has terminated, since the only information about \overline{x}_{i} can be taken from the assumption that associates \overline{x}_{i} to the value of x_{i} at the termination time of Π_{i}.

Please note that the index i is always used if we refer to the role of a process Π_{i} as a deliverer of a result in result_{i} while the index j is used if we refer to the role of some Π_{j} as a receiver of a result in wait_{j}. The details of result_{i} and wait_{j} are described in the next subsection.

5.3 The Detailed Structure

The following global variables are used in the model program for the communication and synchronization between processes:

• value_{i} holds the result of Π_{i} after Π_{i} has terminated. This variable models the value field of a Paclib result descriptor.

• avail_{i} is a boolean flag signalling that value_{i} holds the result of Π_{i}. This variable models the avail field of a Paclib result descriptor.

• W_{i} is a set that holds the identifiers of all processes being blocked on an attempt to receive the result of Π_{i}. This variable models the queue defined by the wait/value fields of a Paclib result descriptor.

• wsem_{i} is a binary semaphore that provides mutual exclusion during the access to W_{i}. This variable models the sem field of a Paclib result descriptor.

• R_{j} is the set that holds all the processes that some Π_{j} waits for. This variable one the one hand is the input argument of the wait_{j} call, on the other hand it models the wait field of a Paclib task descriptor.

• rsem_{j} is a binary semaphore that provides synchronization between all Π_{i} that may deliver their result to Π_{j}. This variable models the sem field of a Paclib task descriptor.

• run_{j} is a binary semaphore used to block a process Π_{j} when none of the Π_{i} with i ∈ \overline{R}_{j} has yet terminated. This variable therefore models the dequeuing of a task descriptor from the scheduling queue.

This model is a simplification of the actual data representation in the Paclib kernel, in particular concerning the following features:

1. Data Structures: The task queue in a Paclib result descriptor and the task list in a Paclib task descriptor are modelled by the mathematical sets W_{i} and R_{j}, respectively. Hence, modifications of queues and lists are modelled by set operations. This may essentially change the semantics of the program as discussed below.

2. Result Descriptor: The value field in a Paclib result descriptor serves as the tail of the wait queue before it actually receives the result of the process. In the model program, this role is played by two distinct variables value_{i} and W_{i}. This also has some crucial consequences on the program model as discussed below.

3. Task Descriptor: When a Paclib task is blocked, the wait field of the task descriptor contains the set of tasks that the blocked task waits for. After it has been awaked, the wait field holds the identifier of the delivering task and the value field holds the result. Since in the model program all variables are globally known to all processes, Π_{i} directly reads R_{j} to determine the processes that Π_{j} is waiting for and writes itself i and x_{i} into r_{j} and y_{j}, respectively. We will ignore this issue in our verification.

4. Life Time: In the model program, all variables have an infinite life time and may be accessed even after some processes have terminated. In the Paclib kernel, the local variables of a process and the contents of a task descriptor may be not accessed any more after the process has terminated since the process workspace has been freed and the contents of the corresponding memory cells are undefined. Since this problem is closely related to many low level details of process creation and termination, we will not deal with it in our verification.

Before we discuss the model in more detail, let us take a look at the internal structure of result_{i} and wait_{j} in Figure 3 and Figure 4, respectively.

• result_{i} first writes the result x_{i} into the variable value_{i} and sets the avail_{i} flag. It then temporarily locks wsem_{i} to receive one process j ∈ W_{i} blocked on an attempt to receive the result of Π_{i}. Afterwards it locks rsem_{j} and determines whether j is still in W_{i} or if another process Π_{i′} has already delivered its result to Π_{j} and has removed j from W_{i}. If j is still in W_{i}, Π_{i} has “won the race” and iteratively removes j from the wait sets W_{i′} of all Π_{i′} that Π_{j} was waiting for. Afterwards, Π_{i} delivers its result to Π_{j}, awakes the task by calling V(run_{j}) and continues the delivery of results until all blocked task have been awaked.

• wait_{j} first locks rsem_{j} to prevent any process Π_{i} from delivering its result to Π_{j} while P i_{j} is not yet blocked. Then Π_{j} iteratively examines the state of each avail_{i} with i ∈ R_{j}. If the avail_{i} flag is not yet set, Π_{j} adds j to the corresponding wait set W_{i} and continues the search. If none of the avail_{i} flags is set, Π_{j} unlocks rsem_{j} and blocks itself by calling P(run_{j}). After it has been awaked by some Π_{i}, the results are available by r_{j} = i and y_{j} = x_{i}. However, if some of the Π_{i} has already delivered its result, Π_{j} itself sets r_{j} and x_{j} and removes j from all W_{i} to which it has added j before.

The algorithm itself reflects more or less the Paclib program given in Appendix A with one major exception: while pacWait fills the value and the avail field of its result descriptor at the end of the program, the function wait_{j} defines value_{j} and avail_{j} at the beginning. The reason for this is the following:

1. pacWait uses the value field to store the tail pointer of the wait queue before the result is available. Since other tasks may remove items from this queue as long as this queue is not empty, the result may be written into the value field only at the end of the function (when all blocked tasks have been processed).

2. It can not be proved that a wait_{j} call always returns on the basis of a pure set interpretation of W_{j} if the value_{i} variable is filled at the end of the program. We either have to add an axiom that asserts that W_{j} fulfills the “first in, first out” property of queues or restructure the program in the presented way.

We will discuss this issue in Section 6.3 in more detail. The last point that we have to mention is the definition of the operations add and rem that are used for operations on the sets W_{j}. In the Paclib kernel, the wait queues in the Paclib result descriptors are the only compound data structures that are modified by different tasks. The purpose of the semaphores in these descriptors is to guarantee the consistent modification of these queues.

However, in our program we have modelled the wait queues as sets W_{j} to which the set operations ∪ and \ may be applied. However, these set operations are atomic and need no protection at all! Even, if we keep the protecting semaphores in the program and prove that they do not cause any harm (like deadlocks), we may and will apply the fact that sets can be atomically updated by one statement.

In order to make the model more realistic, we therefore replace the set operations ∪ and \ on W_{j} by the functions add and rem defined by the following code sequences: resulti(x_{i}) ≡

(α_{1}^{i}) value_{i} := x_{i} (α_{2}^{i}) avail_{i} := true

(α_{3}^{i}) P(wsem_{i}) (α_{4}^{i}) while W_{i} ≠ ∅ do (α_{5}^{i}) w_{i} ∈ W_{i} (α_{6}^{i}) V(wsem_{i})

(α_{7}^{i}) P(rsem_{w_{i}})

(α_{8}^{i}) P(wsem_{i}) (α_{9}^{i}) deliver_{i} := w_{i} ∈ W_{i} (α_{10}^{i}) V(wsem_{i})

(α_{11}^{i}) if deliver_{i} then

(α_{12}^{i}) S_{i} := R_{w_{i}} (α_{13}^{i}) while S_{i} ≠ ∅ do (α_{14}^{i}) s_{i} ∈ S_{i} (α_{15}^{i}) P(wsem_{s_{i}}) (α_{16}^{i}) rem(W_{s_{i}}, w_{i}) (α_{17}^{i}) V(wsem_{s_{i}}) (α_{18}^{i}) S_{i} := S_{i}\{s_{i}}

endwhile

(α_{19}^{i}) y_{w_{i}} := x_{i} (α_{20}^{i}) r_{w_{i}} := i (α_{21}^{i}) V(run_{w_{i}})

endif

(α_{22}^{i}) V(rsem_{w_{i}})

(α_{23}^{i}) P(wsem_{i})

endwhile (α_{24}^{i}) V(wsem_{i})

(α_{e}^{i}) stop

Figure 3: Result Process waitj(y_{j}, r_{j}, R_{j}) ≡

(β_{1}^{j}) P_{j} := R_{j}

(β_{2}^{j}) P(rsem_{j}) (β_{3}^{j}) while P_{j} ≠ ∅ ∧ ¬found_{j} do

(β_{4}^{j}) p_{j} ∈ P_{j} (β_{5}^{j}) P(wsem_{p_{j}})

(β_{6}^{j}) if ¬avail_{p_{j}} then

(β_{7}^{j}) add(W_{p_{j}}, j) (β_{8}^{j}) V(wsem_{p_{j}}) (β_{9}^{j}) P_{j} := P_{j}\{p_{j}}

else

(β_{10}^{j}) V(wsem_{p_{j}})

(β_{11}^{j}) y_{j} := value_{p_{j}} (β_{12}^{j}) r_{j} := p_{j} (β_{13}^{j}) found_{j} := true

(β_{14}^{j}) Q_{j} := R_{j}\P_{j} (β_{15}^{j}) while Q_{j} ≠ ∅ do (β_{16}^{j}) q_{j} ∈ Q_{j} (β_{17}^{j}) P(wsem_{q_{j}}) (β_{18}^{j}) rem(W_{q_{j}}, j) (β_{19}^{j}) V(wsem_{q_{j}}) (β_{20}^{j}) Q_{j} := Q_{j}\{q_{j}}

endwhile endif

endwhile (β_{21}^{j}) V(rsem_{j})

(β_{22}^{j}) if found_{j} then (β_{23}^{j}) found_{j} := false

else (β_{24}^{j}) P(run_{j})

endif

(β_{e}^{j}) nop

Figure 4: Wait Process

(λ_{l}^{p}) add(W, e) ≡
(λ_{l_{a}}^{p}) T_{p} := W
(λ_{l_{b}}^{p}) W := …
(λ_{l_{c}}^{p}) W := T_{p} ∪ {e}
(λ_{l}^{p}) del(W, e) ≡
(λ_{l_{a}}^{p}) T_{p} := W
(λ_{l_{b}}^{p}) W := …
(λ_{l_{c}}^{p}) W := T_{p}\{e}

where T_{p} is a new auxiliary variable. During the execution of these code sequences, there exists one inconsistent state during which we have no information on the value of W. If we are now able to verify the correctness of the model program, we may assume that the inconsistent state during the modifications of the wait queues does not cause any harm. For all other sets, that are either only used by one process or not modified at all, we will use the mathematical set operations.

Finally, let us now define the initialization condition I ∧ J of Π where I defines the initial states of all “result-related” program variables and J defines the initial states of all “waitrelated” variables:

I ≡ ∀i(wsem_{i} ∧ ¬avail_{i} ∧ W_{i} = ∅)
J ≡ ∀j(rsem_{j} ∧ ¬found_{j} ∧ ¬run_{j})

We assume that these variables will be only used within the functions result_{i} and wait_{j} and are in particular not modified elsewhere in Π. The main lines of the proof and the central theorems are presented in the next section.

6 The Verification

In this section, we will present the main lines of the verification of Theorem 1 (Correctness). The proof is based on four central theorems that can be informally described as follows:

1. Theorem 2 (No Result) says that the program flags found_{j} and run_{j} will be never set to true, if no process Π with i ∈ R_{j} terminates.

2. Theorem 3 (Found) says that if Π_{j} has set the found flag, it has itself found the result of some terminated process Π_{i}.

3. Theorem 4 (Awake) says that, if some Π_{i} has set run_{j} to true, Π_{i} has delivered its result to Π_{j}.

4. Theorem 5 (Sometime) says that some Π_{i} will eventually set run_{j} to true, if Π_{j} is blocked.

Please note that Theorem 2, Theorem 3 and Theorem 4 describe invariance properties while Theorem 5 describes an eventuality property of Π .

Theorem 2 is the basis of Proposition 1 (No Result) of the correctness theorem; Theorem 3 and Theorem 4 together establish the correctness of Proposition 2b (Result Delivery); last but not least Theorem 5 is the main constituent of Proposition 2a (Wait Continuation).

In the whole proof, in all theorems and lemmas, we assume that j, τ_{w} ≥ τ_{Π}, \overline{R} and \overline{x} are arbitrary fixed such that

τ_{s} → □∀i(α_{1}^{i} → x_{i} = \overline{x}_{i}), (1) τ_{w} → (β_{1}^{j} ∧ R_{j} = \overline{R}_{j}). (2)

Furthermore, we will use the predicate

elem_{i}(j, W) ≡ (wsem_{i} → j ∈ W) ∧ (¬wsem_{i} → (j ∈ W atnext wsem_{i})). which informally says that, if no process currently updates the set W, j is in W. However, if W is currently modified, then i will be in W when W is consistent again. In general, we use this predicate instead of ∈ to describe properties of W_{i} because an assertion j ∈ W_{i} that has held before W_{i} has been modified and will hold after the modification has been completed does not hold during the modification! In the following three subsections, we will verify the three conclusions of the correctness theorem based on the theorems presented above. We will prove these theorems based on a set of lemmas described and proved in Appendix B. The reader should understand the contents of these lemmas (not their proofs) before reading the following subsections. The proofs of these lemmas actually represent the technically difficult parts of the verification.

6.1 No Result

We will prove Proposition 1 of Theorem 1 (Correctness). We assume that no process in \overline{R}_{j} delivers a result τ_{Π} → ∀i ∈ \overline{R}_{j}(□¬α_{1}^{i}) (3) and want to prove that process j will not return from the wait_{j} call τ_{w} → □¬β_{e}^{j}. (4) By τ_{Π} ≤ τ_{w} and Axiom 3 (Execute), it suffices to prove τ_{Π} → □¬ at{β_{e}^{j}}. (5) By Rule 4 (Induction), we first have to show τ_{Π} → ¬ at{β_{e}^{j}} (6) which is a direct consequence of start_{Π} and Axiom 4 (Two Ready). Now let time τ > τ_{Π} be arbitrary fixed. Assuming τ_{Π} → (¬ at{β_{e}^{j}} until τ) (7) we have to prove τ → ¬ at{β_{e}^{j}}. (8) By the program structure and (7), we may assume τ → △(β_{23}^{j} ∨ β_{24}^{j}). (9) since otherwise (8) is immediately fulfilled. We will now distinguish two cases:

Case τ → △β{j \atop 23}

By Theorem 2 (No Result), we have τ → △¬found_{j}. (10) This, by Lemma 16 (Reset), contradicts the case assumption.

Case τ → △β{j \atop 24}

By Theorem 2 (No Result), we have τ → △¬run_{j}. (11) This, by Axiom 11 (Wait Statement), contradicts the case assumption. □ We will now prove the central theorem of this subsection which says that, if no Π_{i} with i ∈ R_{j} terminates, the flag found_{j} and the binary semaphore run_{j} will be never set.

Theorem 2 (No Result) If no process in \overline{R}_{j} terminates, j will not find a result and be blocked forever i.e.

(τ_{Π} → □∀i ∈ \overline{R}_{j}(¬α_{1}^{i})) → (τ_{Π} → □(¬found_{j} ∧ ¬run_{j})). Proof: Assume τ_{Π} → □∀i ∈ \overline{R}_{j}(¬α_{1}^{i}). (12) By Rule 4 (Induction), we first have to prove τ_{Π} → (¬found_{j} ∧ ¬run_{j}) (13) which is a consequence of start_{Π}. Now let time τ > τ_{Π} be arbitrary fixed. Assuming τ_{Π} → ((¬found_{j} ∧ ¬run_{j}) until τ) (14) we have to prove τ → (¬found_{j} ∧ ¬run_{j}). (15) By the structure of the program, we may assume τ → △(β_{13}^{j} ∨ ∃i(α_{21}^{i} ∧ w_{i} = j)). (16) since these are the only statements modifying found_{j} and run_{j}. However, τ → △β_{13}^{j} contradicts Lemma 10 (If Available) and Lemma 11 (Not Available). Furthermore, τ → △∃i(α_{21}^{i} ∧ w_{i} = j) contradicts by the program structure (12). □

6.2 Result Delivery

We will prove Proposition 2b of Theorem 1 (Correctness). We assume τ_{Π} → ∃i ∈ \overline{R}_{j}(◇α_{1}^{i}). (17) and want to prove τ_{w} → ((r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}) atnext β_{e}^{j}). (18) In case of τ_{w} → □¬β_{e}^{j} (19) we are done. Otherwise, by the program structure there exist times τ_{d}, τ_{e}, τ_{f}, τ_{r} such that τ_{w} → (τ_{d} atnext β_{2}^{j}), (20) τ_{w} → (τ_{e} atnext β_{21}^{j}), (21)

(22) τ_{w} → (τ_{f} atnext at{β_{e}^{j}}), τ_{w} → (τ_{r} atnext β_{e}^{j}). (23) These definitions will be used in this section and all associated lemmas. We now can reformulate (18) as τ_{r} → (r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}). (24) By Axiom 3 (Execute), we know τ_{r} → at{β_{e}^{j}}. (25) We will prove (24) by induction on the number t of times that β_{e}^{r} was not scheduled for execution i.e. on t = τ_{r} − τ_{f}. The base case of the induction τ_{r} = τ_{f} characterized by τ_{r} → △(β_{23}^{j} ∨ β_{24}^{j}) (26) will be shown in the following two subsections. For the induction step, let us assume τ_{r} → △( at\{β_{e}^{j}\} ∧ r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}). (27)

By Lemma 30 (Exit), we also know τ → △∀i( at{α_{6}^{i} … α_{21}^{i}} → w_{i} ≠ j) (28) i.e. r_{j} and y_{j} cannot be modified by any Π_{i}. Therefore we have (24). We will further on deal with the two cases of the induction base.

6.2.1 Case τr → △β{j \atop 23}

By Lemma 16 (Reset), we know τ_{r} → △found_{j}. (29) By Theorem 3 (Found), we then know τ_{r} → △(r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}). (30) By the program structure, we then have (24). We will now prove the first central theorem of this subsection which says that if Π_{j} has set the found_{j} flag it has found the result of some Π with i ∈ R_{j}. Theorem 3 (Found) If j has set the found flag, it has indeed found a result:

τ_{w} → ((found_{j} → (r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}})) until τ_{r}). Proof: Define E ≡ found_{j} → (r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}). (31) By Rule 5 (Bounded Induction), we first have to show τ_{w} → E (32) which is a consequence of Lemma 19 (Entry). Now let τ be arbitrary fixed with τ_{w} < τ < τ_{r} and assume τ_{w} → (E until τ). (33) We have to prove τ → E. (34) We may assume τ → △(β_{11}^{j} ∨ β_{12}^{j} ∨ β_{13}^{j} ∨ ∃i(w_{i} = j ∧ (α_{19}^{j} ∨ α_{20}^{j}))) (35) since these are the only statements modifying y_{j}, r_{j} or found_{j}.

Case τ → △(β{j \atop 11} ∨ β{j \atop 12})

By Lemma 15 (Not Found), we have τ → △¬found_{j} (36) and hence, by the program structure, τ → ¬found_{j}. (37)

Case τ → △β{j \atop 13}

By Lemma 10 (If Available), we know τ → △avail_{p_{j}} (38) and by Lemma 5 (Result Exclusion) τ → △(r_{j} = p_{j}). (39) This implies by Lemma 12 (Process Set) and Lemma 13 (Result) τ → △(r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}). (40) Then we are by the program structure done.

Case τ → △(wi = j ∧ (α{i \atop 19} ∨ α{i \atop 20})) By Lemma 22 (Lock), we know τ → (elem_{i}(j, W_{i}) atprev α_{7}^{i}). (41) Furthermore, by Axiom 11 (Wait Statement) we know τ → (rsem_{j} atprev α_{7}^{i}). (42) This implies by Lemma 28 (Result Loop) τ → ((¬found_{j} ∧ ¬run_{j} ∧ at{β_{22}^{j}, β_{24}^{j}}) atprev α_{7}^{i})). (43) By Lemma 5 (Result Exclusion) and the program structure we then know τ → ¬found_{j}. □ (44)

6.2.2 Case τ → △β{j \atop 24}

By Axiom 11 (Wait Statement), we know τ → △run_{j}. (45) Thus we know by Theorem 4 (Awake) τ → △(r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}) (46) By the program structure, we then have (24). □ We will now prove the second central theorem of this subsection which says that if some Π_{i} sets run_{j} it has delivered its result to Π_{j}. Theorem 4 (Awake) If process j is waked up by some process i, then j has received the result x_{i}:

τ_{w} → ((run_{j} → (r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}})) until τ_{r}). Proof: Define F ≡ run_{j} → (r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{r_{j}}). (47) By Rule 5 (Bounded Induction), we first have to prove τ_{w} → F (48) which is true since Lemma 19 (Entry) implies τ_{w} → ¬run_{j}. Let τ be arbitrary fixed with τ_{w} < τ < τ_{r} and assume τ_{w} → (F until τ). (49) We have to prove τ → F. (50) We may assume τ → △(β_{11}^{j} ∨ β_{12}^{j} ∨ ∃i(w_{i} = j ∧ (α_{19}^{i} ∨ α_{20}^{i} ∨ α_{21}^{i}))) (51) since these are the only statements that may modify y_{j}, r_{j} or run_{j}.

Case τ → △(β{j \atop 11} ∨ β{j \atop 12})

By τ < τ_{e}, Lemma 23 (Not Run) implies τ → △¬run_{j}. (52) By the program structure, we thus have τ → ¬run_{j}. (53)

Case τ → △(wi = j ∧ (α{i \atop 19} ∨ α{i \atop 20})) Lemma 22 (Lock) implies τ → (elem_{i}(j, W_{i}) atprev α_{7}^{i}). (54) By Axiom 11 (Wait Statement), we know τ → (rsem_{j} atprev α_{7}^{i}). (55) By Lemma 28 (Result Loop), we thus know τ → (¬run_{j} atprev α_{7}^{i}). (56) This implies by Lemma 5 (Result Exclusion) τ → ¬run_{j}. (57)

Case τ → △(wi = j ∧ α{i \atop 21}) By the structure of the program and Lemma 5 (Result Exclusion), we know τ → △(r_{j} = i ∧ y_{j} = \overline{x}_{i}). (58) By Lemma 22 (Lock), we then know τ → (elem_{i}(j, W_{i}) atprev α_{7}^{i}). (59) which implies by Lemma 20 (Membership) τ → (i ∈ \overline{R}_{j} atprev α_{7}^{i}) (60) and thus by Lemma 8 (Constancy) τ → △(i ∈ \overline{R}_{j}). (61) This implies by the program structure τ → (r_{j} ∈ \overline{R}_{j} ∧ y_{j} = \overline{x}_{j}). □ (62)

6.3 Wait Continuation

We are going to prove Proposition 2a of Theorem 1 (Correctness). We assume τ_{Π} → ∃i ∈ \overline{R}_{j}(◇ at\{α_{1}^{i}\}) (63) and have to prove τ_{w} → ◇ at{β_{e}^{j}}. (64) By Lemma 31 (Wait Continuation) and Lemma 35 (Result Continuation), we know τ_{w} → ◇β_{21}^{j}. (65) We thus may define some time τ_{e} > τ_{w} such that τ_{w} → (τ_{e} atnext β_{21}^{j}). (66)

We may assume τ_{e} → ¬found_{j} (67) since otherwise, by Lemma 1 (Locality) and the program structure, we are done. Thus we know τ_{e} → ◇ at{β_{24}^{j}} (68) and have to show τ_{e} → (◇run_{j} atnext β_{24}^{j}). (69) From (67) we know by Lemma 26 (Wait End) τ_{e} → ∀i ∈ \overline{R}_{j}(elem_{i}(j, W_{i})) (70) By the program structure, we also know τ_{e} → ^{◯}rsem_{j} (71) which implies by Theorem 5 (Sometime) τ_{e} → ^{◯}◇run_{j} (72) and, since run_{j} is nowhere else set to false, (69). □ The following theorem says that, if Π_{j} has put j into some W_{i}, some Π_{i} will eventually set run_{j}. Theorem 5 (Sometime) If j is in some W_{i}, run_{j} will be eventually set.

τ_{w} → (((rsem_{j} ∧ ∃i(elem_{i}(j, W_{i}))) → ◇run_{j}) until τ_{r}). Proof: Let τ ≥ τ_{w} be arbitrary fixed and assume for some i τ → (rsem_{j} ∧ elem_{i}(j, W_{i})). (73) By Lemma 21 (Waiting), we know τ → at{β_{22}^{j} … β_{e}^{j}}. (74) By Lemma 38 (Result Induction), we know τ_{e} → ◇(α_{4}^{i} ∧ W_{i} = ∅). (75) By (74) and the program structure, we know for some i′ ∈ \overline{R}_{j} τ_{e} → ◇(α_{16}^{i′} ∧ s_{i′} = i ∧ w_{i′} = j). (76) This implies τ_{e} → ◇(α_{21}^{i′} ∧ w_{i′} = j) (77) and we are by the program structure done. □ The proof of the previous theorem is essentially based on Lemma 38 (Result Induction) saying that result_{i} always terminates. This lemma holds since result_{i} defines value_{i} and sets the flag avail_{i} i.e. before it starts to deliver its result to other tasks. Please note that this is not true in the actual implementation of pacWait where avail_{i} is set after the result has been delivered. However, if we add the following axiom that demands a queue interpretation of W_{i}, Theorem 5 (Sometime) is true again. Axiom 18 (Queue) W_{i} is accessed in a first in/first out manner:

τ_{Π} → □∀i∀j∀j′((elem_{i}(j, W_{i}) ∧ ¬elem_{i}(j′, W_{i})) →

(¬elem_{i}(j, W_{i}) before ¬elem_{i}(j′, W_{i}))).

By this axiom, we may use Lemma 39 (First Out) to verify Theorem 5 (Sometime):

Proof: Let τ ≥ τ_{Π} be arbitrary fixed and assume for some i

τ → (rsem_{j} ∧ elem_{i}(j, W_{i})). (78)

By Lemma 21 (Waiting), we know

τ → at{β_{22}^{j} … β_{e}^{j}}. (79)

By Lemma 39 (First Out), we know

τ → ◇¬elem_{i}(j, W_{i}). (80)

By (79) and the program structure, we know for some i′ ∈ \overline{R}_{j}

τ_{e} → ◇(α_{16}^{i′} ∧ s_{i′} = i ∧ w_{i′} = j). (81)

This implies

τ_{e} → ◇(α_{21}^{i′} ∧ w_{i′} = j) (82)

and we are by the program structure done. □

7 Conclusions

We conclude this paper by summarizing the basic proof techniques that we have applied in the program verification. For the semi-formal reasoning process, we usually used the generalized induction rule introduced in this paper.

1. Locality: If parts of a program only operate on local variables (i.e. variables that are only modified by the current process), these program parts can be verified without considering the existence of other processes. The complexity of the verification is thus essentially decreased.

2. Program Variables: Whenever possible we have expressed program properties in terms of program variables instead of program locations. For instance, Theorem 3 (Found) and Theorem 4 (Awake) are formulated using the variables found_{j} and run_{j} and not the program locations β_{23}^{j} and β_{24}^{j}, respectively. Thus the propositions become more easy to understand and express the intuitions of the programmer better than by dealing with program locations. This is especially of advantage when code blocks are rearranged such that the locations of statements change but the proposition in terms of program variables still holds.

3. Critical Regions: The purpose of a critical region C

(λ_{a}) P(sem)

C

(λ_{b}) V(sem)

is described by a proposition of the form

□(sem → A)

saying that A holds when no process is within C and therefore also when a process enters respectively exits C. For proving above formula, we have to prove τ_{Π} → A and, for some arbitrary fixed time τ > τ_{Π},

τ → (λ_{b} → ^{◯}A)

i.e. that the A holds when C is left. For the proof of this proposition, one may assume the induction hypothesis

τ → (A atprev τ_{a})

i.e. that A was true when C was entered. The reasoning from τ_{a} to τ_{e} may be based on the fact that no other process is in C. Furthermore, we have to prove for each statement λ in every other process

(λ ∧ sem ∧ A) → ^{◯}A

where we may restrict our consideration to those λ that might change the truth value of A (e.g. by modifying some program variable occurring in A).

4. While Loops: The invariant of a loop

(λ′) …

(λ) while B do

…

(λ′′) … endwhile

is expressed by a proposition of the form

□( at{λ} → A)

which says that A always holds when execution is at the location λ. For proving this formula, we have to prove

□(λ′ → ^{◯}A)

i.e. that A holds when the loop is entered for the first time and

( at{λ} ∧ ¬λ ∧ A) → ^{◯}A

i.e. A does not become false if some other process is executed (where we may restrict considerations to those statements in other processes that may affect A) and

λ′′ → ^{◯}A

i.e. A holds after each iteration. For proving this fact, we may apply the induction hypothesis

λ′′ → (A ∧ B atprev λ)

and then reason from one execution of λ to the next.

5. Nested Loops: The invariants A_{1} and A_{2} of two nested loops

(λ_{1}) while B_{1} do … (λ_{2}) while B_{2} do

… endwhile … endwhile

can be only verified by forming a joint invariant

A ≡ ( at{λ_{1}} → A_{1}) ∧ ( at{λ_{2}} → A_{2})

and proving this joint proposition at all interesting transitions. A may be assumed for all former time moments (similar to the case of a single while loop).

6. Critical Loops: If the entry of a loop is part of a critical region

P(sem) (λ) while B do

… V(sem) … P(sem) endwhile V(sem)

the loop invariant actually reduces to the invariant of the critical region protected by sem extended by the proposition B i.e.

□(sem ∧ B → A)

and then proceeds in a way similar to simple while loops.

7. Continuation: A good strategy to verify the continuation of a program is to verify the freedom of deadlocks of critical regions and the termination of loops from inside to the outside starting with the innermost region/loop. Parallel programs are usually constructed in such a way that there exists a partial ordering ≺ on semaphores such that s_{1} ≺ s_{2} implies that a critical region protected by s_{1} is only entered if the process is not in a critical region protected by s_{2}. This ordering also guides the structure of the proof.

There can be no general recipe how the verification of a parallel program with shared variables has to be organized to be manageable but also convincing. In the worst case, all parallel processes may be coupled so tightly that the full calculus of temporal logic has to be applied by constructing for every statement in every process an assertion that describes the full state of the program. Each of these assertions has then to be verified against every statement.

However, such situations probably occur very rarely. In many cases, the verification style presented in this paper may save a considerable amount of work and make the verification a valuable documentation of the program. A high-level parallel programming model should be constructed in such a way that the model is powerful enough to express the parallel algorithms one is interested in but also restricted enough to cut down the complexity of parallel program verification.

References

[CM88] Mani K. Chandy and Jayadev Misra. Parallel Program Design — A Foundation. Addison-Wesley, Reading, Massachusetts, 1988.

[Hoa85] C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ, 1985.

[HSN^{+}92] Hoon Hong, Wolfgang Schreiner, Andreas Neubacher, Kurt Siegl, Hans-Wolfgang Loidl, Tudor Jebelean, and Peter Zettler. PACLIB User Manual. Technical Report 92-32, RISC-Linz, Johannes Kepler University, Linz, Austria, May 1992. Also: Technical Report 92-9, ACPC Technical Report Series, Austrian Center for Parallel Computation, July 1992.

[Krö87] Fred Kröger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer, Berlin, 1987.

[Mil80] Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980.

[Mil93] Robert Milner. Elements of Interaction. Communications of the ACM, 36(1):78– 89, January 1993.

[MP81] Z. Manna and Z. Pnueli. Verification of Concurrent Programs, Part 1: The Temporal Framework. Technical Report STAN-CS-81-836, Stanford University, Palo Alto, CA, June 1981.

[OG76] S. Owicki and D. Gries. Verifying Properties of Parallel Programs: An Axiomatic Approach. Communications of the ACM, 19(5):279–285, May 1976.

[OL82] S. Owicki and L. Lamport. Proving Liveness Properties of Parallel Programs: An Axiomatic Approach. ACM Transactions on Programming Languages and Systems, 4(3):455–495, July 1982.

[Oss83] Marty Ossefort. Correctness Proofs of Communicating Processes: Three Illustrative Examples from the Literature. ACM Transactions on Programming Languages and Systems, 5(4):620–640, October 1983.

[Sch92] Wolfgang Schreiner. The Design of the PACLIB Kernel. Technical Report 92-33, RISC-Linz, Johannes Kepler University, Linz, Austria, 1992.

A The PACLIB Kernel

/*****************************************************************************/
void pacShell(pacFunction f,
pacObject a1, pacObject a2, pacObject a3, pacObject a4,
pacObject a5, pacObject a6, pacObject a7, pacObject a8) {
/*****************************************************************************/
pacResult(f(a1, a2, a3, a4, a5, a6, a7, a8));
pacDie();
}
/*****************************************************************************/
void pacResult(pacObject v) {
/*****************************************************************************/
pacObject value, value0;             /* function results */
pacTask result, result0;             /* result descriptor */
pacTaskList rlist;                   /* list of result descriptors */
pacTaskList tlist, tlist0, tlist1;   /* lists of task descriptors*/
uTask task, task0;                   /* task descriptors */
int deliver;                         /* deliver flag */
result = uWorkTask->pac.result;      /* result descriptor of current task */
resLock(result);                     /* lock descriptor */
resGet(result, &task0, &value, &tlist); /* get associated task list */
while (!listNull(tlist)) {           /* there are some waiting tasks */
  task = (uTask)listHead(tlist);     /* get next waiting task */
  resUnlock(result);                 /* unlock result descriptor */
  taskLock(task);                    /* lock task descriptor */
  resLock(result);                   /* lock descriptor again */
  resGet(result, &task0, &value, &tlist);
  deliver = (!listNull(tlist)) && ((uTask)listHead(tlist) == task);
  resUnlock(result);                 /* unlock descriptor again */
  if (deliver) {                     /* remove task from result descr */
    rlist = task->pac.wait;          /* results the task waited for */
    while (!listNull(rlist)) {       /* remove task from result descs */
      result0 = listHead(rlist);     /* get next result descriptor */
      resLock(result0);              /* lock result descriptor */
      resGet(result0, &task0, &value0, &tlist0);
      tlist1 = listNew();            /* empty predecessor list */
      while (task != (uTask)listHead(tlist0)) { /* search for task */
        tlist1 = tlist0;             /* new predecessor */
        tlist0 = listTail(tlist0);   /* task descriptor not yet found */
      }
      if (listNull(tlist1))          /* head of queue must be updated */
        resSetWait(result0, listTail(tlist0));
      else                           /* unlink the task from the queue */
        listSetTail(tlist1, listTail(tlist0));
      if (value0 == tlist0)          /* last task in list removed */
        resSetValue(result0, tlist1);
      resUnlock(result0);            /* unlock result descriptor */
      rlist = listTail(rlist);       /* get next descriptor */

44 A The PACLIB Kernel

    }
    task->pac.wait = result;         /* deliver result descriptor */
    task->pac.value = v;             /* deliver actual result value */
    uWakeTask(task);                 /* wake up task */
  }
  taskUnlock(task);                  /* unlock this task */
  resLock(result);                   /* lock result descriptor */
  resGet(result, &task0, &value, &tlist); /* get associated task list */
}
/* deliver result */
resSetTask(result, AVAILABLE);       /* no task is executing any more */
resSetValue(result, v);              /* this is the result value */
resSetWait(result, NIL);             /* no tasks waiting any more */
resUnlock(result);                   /* unlock result descriptor */
}
/*****************************************************************************/
pacObject pacWaitList(pacTask *tp, pacTaskList rlist) {
/*****************************************************************************/
pacTaskList rlist0;                  /* temp. list of result descriptors */
pacTask result;                      /* actual result descriptor */
uTask task;                          /* actual usystem task */
pacObject value, v;                  /* actual result values */
pacTaskList tlist, tlist0;           /* lists of waiting tasks */
pacObject new;                       /* new list cell */
int found = FALSE;                   /* value was found */
taskLock(uWorkTask);                 /* lock this task */
rlist0 = rlist;                      /* list of result descriptors */
while (!listNull(rlist0) && !found) { /* still more tasks to wait for */
  result = listHead(rlist0);         /* next result descriptor */
  resLock(result);                   /* lock descriptor and get values */
  resGet(result, &task, &value, &tlist);
  if (!taskAvail(task)) {            /* result not available */
    new = listCons((pacObject)uWorkTask, listNew());
    resSetValue(result, new);        /* tail of waiting queue */
    if (listNull(value))             /* no waiting tasks yet */
      resSetWait(result, new);       /* head of waiting queue */
    else                             /* there are already waiting tasks */
      listSetTail(value, new);       /* update tail of waiting queue */
    resUnlock(result);               /* unlock result descriptor */
    rlist0 = listTail(rlist0);       /* get rest of result descriptor list */
    continue;                        /* continue next loop iteration */
  }
  /* task has already terminated and delivered result */
  resUnlock(result);                 /* unlock descriptor */
  if (tp) *tp = result;              /* remember result descriptor */
  v = value;                         /* result value */

found = TRUE;                      /* value was found */
while(rlist != rlist0) {           /* remove task from descriptors again */
  result = listHead(rlist);        /* next result descriptor */
  resLock(result);                 /* lock descriptor */
  resGet(result, &task, &value, &tlist);
  tlist0 = listNew();              /* predecessor in list */
  while ((uTask)listHead(tlist) != uWorkTask) {
    tlist0 = tlist;                /* new predecessor */
    tlist = listTail(tlist);       /* next list tail */
  }
  if (listNull(tlist0))            /* no predecessor in list */
    resSetWait(result, listTail(tlist));
  else                             /* predecessor in list */
    listSetTail(tlist0, listTail(tlist));
  if (value == tlist) resSetValue(result, tlist0);
  resUnlock(result);               /* unlock result descriptor */
  rlist = listTail(rlist);         /* rest of list */
}
}
if (found)                           /* value was found */
taskUnlock(uWorkTask);             /* unlock current task */
else {                               /* value not found */
uWorkTask->pac.wait = rlist;       /* list of results that we wait for */
taskUnlock(uWorkTask);             /* unlock current task */
uBlockTask();                      /* block current task */
if (tp) *tp = uWorkTask->pac.wait; /* this is the result descriptor */
v = uWorkTask->pac.value;          /* this is the actual result */
uWorkTask->pac.wait = listNew();   /* reset wait field */
uWorkTask->pac.value = listNew();  /* reset value field */
}
return(v);                           /* return result */
}

\underline{46 B Lemmas}

B Lemmas

We now list all auxiliary lemmas classified into the following categories:

1. Mutual Exclusion Lemmas restricting the access to program regions and data structures.

2. Operation Lemmas describing the validity and the effects of several program operations.

3. Structure Lemmas describing properties that can be derived from the static structure of the program.

4. Main Lemmas that essentially capture the dynamic behavior of the program.

5. Continuation Lemmas that describe eventuality properties of the program.

The lemmas are listed in a bottom-up order i.e. the proof of a lemma is based only on previously listed lemmas (with some explicitly mentioned exceptions).

B.1 Mutual Exclusion Lemmas

We define the predicate invar(a) by

invar(a) ≡ ∀\overline{a}(a = \overline{a} → ^{◯}a = \overline{a})

saying “a is not changed in the current time moment” and the propositional operator exor({A_{1}, …, A_{n}})

exor({A_{1}, …, A_{n}}) ≡ (A_{1} ∧ ¬A_{2} ∧ … ∧ ¬A_{n})∨
(¬A_{1} ∧ A_{2} ∧ … ∧ ¬A_{n})∨
…
(¬A_{1} ∧ ¬A_{2} ∧ … ∧ A_{n})

saying “exactly one of A_{1}, …, A_{n} is true”.

The following lemma declares a set of program variables to be “local”.

Lemma 1 (Locality) The variables w_{i}, S_{i}, s_{i}, value_{i}, avail_{i}, deliver_{i}, P_{j}, p_{j}, Q_{j}, q_{j} and found_{j} are only modified by the processes i and j, respectively:

τ_{Π} → □∀i∀i′∀l((λ_{l}^{i′} ∧ i′ ≠ i) →

(invar(w_{i}) ∧ invar(S_{i}) ∧ invar(s_{i}) ∧

invar(value_{i}) ∧ invar(avail_{i}) ∧ invar(deliver_{i})))

τ_{Π} → □∀j∀j′∀l((λ_{l}^{j′} ∧ j′ ≠ j) →

(invar(P_{j}) ∧ invar(p_{j}) ∧ invar(Q_{j}) ∧ invar(q_{j}) ∧ invar(found_{j})))

Proof: These variables are only modified in result_{i} and wait_{j}, respectively. □

The following lemma declares the mutual exclusion of several critical regions protected by the semaphore wsem_{i}. If wsem_{i} is true, no process is within the denoted regions; if wsem_{i} is false, exactly one process is in one of these regions. Please not that only one critical regions is “statically defined” by the structure of the program (i.e. by the value of the location counter of a process), while the others depend on the contents of the program variables s_{i′} and p_{j}, respectively.

Lemma 2 (Wait Semaphore) The family of semaphores wsem_{i} establishes the mutual exclusion of several critical regions:

τ_{Π} → □∀i(exor{
wsem_{i},
at{α_{4}^{i} … α_{6}^{i}, α_{9}^{i}, α_{10}^{i}, α_{24}^{i}},
s_{1} = i ∧ at{α_{16}^{1}, α_{17}^{1}},
…
s_{n} = i ∧ at{α_{16}^{n}, α_{17}^{n}},
p_{1} = i ∧ at{β_{6}^{1} … β_{8}^{i}, β_{10}^{i}},
…
p_{n} = i ∧ at{β_{6}^{n} … β_{8}^{n}, β_{10}^{n}},
q_{1} = i ∧ at{β_{18}^{1} … β_{19}^{1}},
…
q_{n} = i ∧ at{β_{18}^{n} … β_{19}^{n}}}).

Proof: Proving this “obvious” program property is a basically simple but practically tedious task. By Lemma 2 (Invariant Rule), it suffices to show that mutual exclusion holds initially (which is a consequence of start_{Π}) and that it is invariant under each action λ.

Since s_{i}, p_{j} and q_{j} are local to process i and j respectively and s_{i}, p_{j} and q_{j} are not changed within the critical regions, it suffices to check the invariance of the property at the entries and the exits of the critical regions:

1. λ ∈ {α_{3}^{i}, α_{6}^{i}, α_{8}^{i}, α_{10}^{i}, α_{23}^{i}, α_{24}^{i}},

2. λ ∈ {α_{15}^{i′}, α_{17}^{i′}} assuming s_{i′} = i,

3. λ ∈ {β_{5}^{j}, β_{8}^{j}, β_{10}^{j}} assuming p_{j} = i and

4. λ ∈ {β_{17}^{j}, β_{19}^{j}} assuming p_{j} = i.

The details are left to the reader. □

The previous lemma only describes the low-level effect of the semaphore wsem_{i}; its high-level purpose (the protection of the set W_{i}) is actually expressed by the following lemma.

Lemma 3 (Wait Exclusion) Each wait set W_{i} is only modified in a critical region protected by wsem_{i}:

τ_{Π} → □∀i(wsem_{i} → invar(W_{i})).

Proof: This is a corollary of Lemma 2 (Wait Semaphore) (check!). □

Likewise, we define the effect and the purpose of the semaphore rsem_{j}.

Lemma 4 (Result Semaphore) The family of semaphores rsem_{j} establishes the mutual exclusion of several critical regions:

τ_{Π} → □∀j(exor{
rsem_{j},
at{β_{3}^{j} … β_{21}^{j}},
w_{1} = j ∧ at{α_{8}^{1} … α_{22}^{1}},
…
w_{n} = j ∧ at{α_{8}^{n} … α_{22}^{n}}}).

Proof: The proof proceeds analogously to the proof of Lemma 2 (Wait Semaphore) by checking that mutual exclusion holds initially (which is a direct consequence of A) and that this property is invariant under the following actions λ:

1. λ ∈ {β_{2}^{j}, β_{21}^{j}} and

2. λ ∈ {α_{7}^{i}, α_{22}^{i}} (assuming w_{i} = j).

The details are left to the reader. □

Lemma 5 (Result Exclusion) The following actions are only performed within a critical region protected by rsem_{j}:

1. y_{j} is modified.

2. r_{j} is modified.

3. run_{j} is set to true.

4. j is added to or removed from some W_{i}.

Formally,

τ_{Π} → □(rsem_{j} →
invar(y_{j}) ∧ invar(r_{j}) ∧ invar(run_{j}) ∧
∀i(elem_{i}(j, W_{i}) ↔ ^{◯}elem_{i}(j, W_{i}))).

Proof: This is a corollary of Lemma 4 (Result Semaphore), Lemma 2 (Wait Semaphore) and the program structure. □

B.2 Operation Lemmas

The effect of the operations add and rem on W_{i} is described by the following lemma.

Lemma 6 (Set Update) If W_{i} is updated by adding or removing some j, then the update has achieved a consistent state at the end of the corresponding critical region:

□∀i∀j∀k∀\overline{W} (
((α_{15}^{i} ∧ W_{i} = \overline{W} ∧ w_{i} = j) → (W_{i} = \overline{W} \\{j\} atnext α_{17}^{i})) ∧
((β_{5}^{j} ∧ p_{j} = k ∧ W_{k} = \overline{W} ∧ ¬avail_{k}) → (W_{k} = \overline{W} ∪ \{j\} atnext β_{8}^{j})) ∧
((β_{17}^{j} ∧ q_{j} = k ∧ W_{k} = \overline{W}) → (W_{k} = \overline{W} \\{j\} atnext β_{19}^{j}))).

Proof: By Lemma 2 (Wait Semaphore). □

The following lemma guarantees that we are allowed to use the ∈ assignment in the program model.

Lemma 7 (Element) The ∈ assignment is well-defined:

τ_{Π} → □∀i((α_{5}^{i} → W_{i} ≠ ∅) ∧ (α_{14}^{i} → S_{i} ≠ ∅)),
τ_{Π} → □((β_{4}^{j} → P_{j} ≠ ∅) ∧ (β_{16}^{j} → Q_{j} ≠ ∅)).

Proof: Lemma 2 (Wait Semaphore) and Axiom 14 (While Loop) imply

τ_{Π} → □∀i(α_{5}^{i} → W_{i} ≠ ∅).

The rest is a consequence of Lemma 1 (Locality) and Axiom 14 (While Loop). □

B.3 Structure Lemmas

The following lemma tells us that in certain contexts we need not distinguish between x_{i} and x̄_{i} and between R_{j} and R̄_{j}:

Lemma 8 (Constancy) The parameters x_{i} and R_{j} are not changed in result_{i} and wait_{j}, respectively:

τ_{Π} → □∀i(α_{1}^{i} → □(x_{i} = \overline{x}_{i})) ∧
τ_{w} → ((R_{j} = \overline{R}_{j} until τ_{r}) ∧ (R_{j} = \overline{R}_{j} atnext τ_{r})).

Proof: By the structure of the program. □

The following lemmas describe the state of several program variables at certain program locations.

Lemma 9 (Available) After the available flag is set, it remains true in result_{i}:

τ_{Π} → □∀i( at{α_{3}^{i} … α_{e}^{i}} → avail_{i}). Proof: By Lemma 1 (Locality). □ Lemma 10 (If Available) In the else branch of wait_{j}, avail_{p_{j}} always holds:

τ_{Π} → □∀j( at{β_{10}^{j} … β_{20}^{j}} → avail_{p_{j}}). Proof: By Axiom 12 (Two Branch Conditional) and Lemma 1 (Locality). □ Lemma 11 (Not Available) If process i does not deliver a result, avail_{i} will never hold:

τ_{Π} → ∀i(□¬ at{α_{1}^{i}} → □¬avail_{i}). Proof: By Rule 4 (Induction). □ Lemma 12 (Process Set) Within wait_{j}, the variables p_{j} and r_{j} are always members of the process set \overline{R}_{j}:

τ_{Π} → □(( at\{β_{5}^{j} … β_{20}^{j}\} → p_{j} ∈ \overline{R}_{j}) ∧ ( at\{β_{17}^{j} … β_{20}^{j}\} → q_{j} ∈ \overline{R}_{j}). Proof: By Rule 4 (Induction). □ Lemma 13 (Result) If the available flag is set, then the result is indeed available:

τ_{Π} → □∀i(avail_{i} → value_{i} = \overline{x}_{i}). Proof: By Rule 8 (Constancy) using that only α_{2}^{i} sets avail_{i} to true. □ Lemma 14 (Found) After found_{j} is set to true, it remains true:

τ_{Π} → □( at{β_{14}^{j} … β_{20}^{j}} → found_{j}). Proof: By Lemma 1 (Locality) and the structure of t eh program. □ Lemma 15 (Not Found) Before found_{j} is set to true, found_{j} is false:

τ_{Π} → □( at{β_{4}^{j} … β_{13}^{j}} → ¬found_{j}). Proof: By Axiom 14 (While Loop) and Lemma 1 (Locality). □ Lemma 16 (Reset) If found_{j} is set to false, it was true before:

τ_{Π} → □( at{β_{23}^{j}} → found_{j}). Proof: By Axiom 12 (Two Branch Conditional) and Lemma 1 (Locality). □ Lemma 17 (Sleeping) If j is going to sleep, found_{j} is false.

τ_{Π} → □( at{β_{24}^{j}} → ¬found_{j}). Proof: By Axiom 12 (Two Branch Conditional) and Lemma 1 (Locality). □ Lemma 18 (Deliver) If process i is in the “then” branch of result_{i}, then deliver_{i} was set at the previous α_{9}^{i}:

τ_{Π} → □∀i( at{α_{12}^{i} … α_{21}^{i}} → (deliver_{i} ∧ w_{i} ∈ W_{i} atprev α_{9}^{i})). Proof: This is a consequence of Axiom 13 (One Branch Conditional) and Lemma 1 (Locality). □

B.4 Main Lemmas

In this section, we give the key lemmas that capture the dynamic behavior of the program. The organization of these lemmas is as follows:

1. Entry: Lemma 19 describes the state of Π when wait_{j} is entered (i.e. it is of the form τ_{w} → A).

2. Others: Most lemmas capture the behavior of Π during the execution of wait_{j} (i.e. they are of the form τ_{w} → (A until τ_{r})).

3. Exit: Lemma 30 describes the state of Π immediately before wait_{j} is left (i.e. it is of

the form τ_{f} → (A until τ_{r}). For proving these lemmas, we perform an induction over the number of times that wait_{j} has been executed before:

1. Induction Base: We prove that Lemma 19 holds when wait_{j} is entered for the first time i.e. has not been executed before.

2. Others: Based on the induction hypothesis Lemma 19, we prove that the other lemmas hold.

3. Exit: Based on the other lemmas, we prove that Lemma 30 holds.

4. Induction Step: based on Lemma 30, we prove that Lemma 19 holds when wait_{j} is

entered for the next time. Both the induction base and the induction step are given in the proof of Lemma 19 (Entry) while the other proofs are listed after the corresponding lemmas. Please note that the use of Lemma 19 in the Lemma 30 is therefore not a vicious circle but a valid assumption in the induction step. Lemma 19 (Entry) When wait_{j} is entered, found_{j} and run_{j} are false and j is not in any wait set W_{i} and no process i is going to deliver its result to j:

t_{w} → (¬found_{j} ∧ ¬run_{j} ∧ ∀i(¬elem_{i}(j, W_{i}) ∧ ( at{α_{12}^{i} … α_{21}^{i}} → w_{i} ≠ j))). Proof: We will prove this lemma by induction over the number of times that wait_{j} has been executed. Define B ≡ ¬found_{j} ∧ ¬run_{j} ∧ ∀i(¬elem_{i}(j, W_{i}) ∧ ( at{α_{12}^{i} … α_{21}^{i}} → w_{i} ≠ j)). (1) We will prove τ_{w} → B. (2)

Induction Base We assume that wait_{j} is entered for the first time i.e. τ_{Π} → (τ_{w} atnext β_{1}^{j}). (3) By start_{Π}, we know τ_{Π} → B. (4) Since only wait_{j} sets found_{j} to true and extends W_{i} by j, we therefore know τ_{w} → (¬found_{j} ∧ ∀i(¬elem_{i}(j, W_{i}))) (5) and also τ_{Π} → ((¬found_{j} ∧ ∀i(¬elem_{i}(j, W_{i}))) until τ_{w}). (6)

From this, we know τ_{Π} → (∀i( at{α_{12}^{i} … α_{21}^{i}} → w_{i} ≠ j) until τ_{w}) (7) which implies τ_{w} → (¬run_{j} ∧ ∀i( at{α_{12}^{i} … α_{21}^{i}} → w_{i} ≠ j)). (8)

Induction Step Let τ′_{w} such that τ_{w} → (τ′_{w} atnext β_{1}^{j}). (9) From Lemma 30 (Exit), we know τ_{r} → B. (10) Since only wait_{j} sets found_{j} to true and extends W_{i} by j, it is easy to derive τ′_{w} → B. (11) Therefore we are done. □ The following lemma establishes a relationship between W_{i} and R_{j}. Lemma 20 (Membership) If process j is in the wait set W_{i}, then process i is in the process set \overline{R}_{j} and j executed wait_{j}:

τ_{w} → ∀i(elem_{i}(j, W_{i}) → i ∈ \overline{R}_{j}) until τ_{r}. Proof: Let i be arbitrary fixed. We know from Lemma 19 (Entry) τ_{w} → ¬elem_{i}(j, W_{i}). (1) Now let τ be arbitrary fixed with τ_{w} < τ < τ_{r} such that τ → elem_{i}(j, W_{i}). (2) By the program structure, we know that for some τ_{p} with τ_{r} < τ_{p} < τ τ_{p} → β_{7}^{j} ∧ p_{j} = i. (3) By Lemma 12 (Process Set), we then know τ_{p} → i ∈ \overline{R}_{j} (4) and by Lemma 8 (Constancy) we are done. □ The following lemma will be used to guarantee that no Π_{i} delivers a result to Π_{j} “too early”. Lemma 21 (Waiting) If outside the critical region protected by rsem_{j} j is in some wait set W_{i}, then process j is ready to receive a result.

τ_{w} → ((rsem_{j} ∧ elem_{i}(j, W_{i})) → at{β_{22}^{j}, β_{e}^{j}}) until τ_{r} Proof: Let τ ≥ τ_{w} be arbitrary fixed such that τ → (rsem_{j} ∧ elem_{i}(j, W_{i})). (1) By Lemma 19 (Entry), we know τ_{w} → ∀i(¬elem_{i}(j, W_{i})) until τ_{d}. (2) By Lemma 4 (Result Semaphore), we know τ_{d} → ¬rsem_{j} until τ_{e}. (3) We therefore know τ > τ_{d}, and thus τ_{d} → at{β_{22}^{j} … β_{e}^{j}}. □ (4) The next lemma fixes a non-obvious property at the start of the critical region protected by rsem_{j}.

Lemma 22 (Lock) If i is going to deliver its result to j then j was in the wait set of i when i locked the critical region protected by rsem_{j}:

τ_{Π} → □∀i(( at{α_{12}^{i} … α_{21}^{i}} ∧ w_{i} = j) → (elem_{i}(j, W_{i}) atprev α_{7}^{i})). Proof: Let i be arbitrary fixed and define D ≡ ∀i(( at{α_{12}^{i} … α_{21}^{i}} ∧ w_{i} = j) → (elem_{i}(j, W_{i}) atprev α_{7}^{i})). (1) From start_{Π}, we know τ_{Π} → D. (2) Let time τ > τ_{Π} be arbitrary fixed such that τ → ( at{α_{12}^{i} … α_{21}^{i}} ∧ w_{i} = j). (3) By Lemma 18 (Deliver), we know τ → (j ∈ W_{i} atprev α_{9}^{i}). (4) By Lemma 2 (Wait Semaphore), we then know τ → (j ∈ W_{i} atprev α_{8}^{i}). (5) By Lemma 5 (Result Exclusion), we then know τ → (elem_{i}(j, W_{i}) atprev α_{7}^{i}). □ (6)

The following lemma guarantees that no Π_{i} delivers a result to Π_{j} before Π_{j} has left the critical region protected by rsem_{j}. Lemma 23 (Not Run) After the entry of wait_{j}, run_{j} remains false until the end of the critical region protected by rsem_{j}:

τ_{w} → (¬run_{j} until τ_{e}). Proof: By Lemma 19 (Entry), we know τ_{w} → ¬run_{j}. (1) By Lemma 19 (Entry) and the program structure, we also know τ_{w} → (∀i(¬elem_{i}(j, W_{i})) until β_{3}^{j}). (2) By Axiom 11 (Wait Statement), we know τ_{w} → (¬rsem_{j} atnext β_{3}^{j}). (3) Moreover, we know by Lemma 22 (Lock) and Axiom 11 (Wait Statement) τ_{w} → ((rsem_{j} ∧ elem_{i}(j, W_{i})) before (α_{21}^{i} ∧ w_{i} = j)). (4) By Lemma 4 (Result Semaphore), (2), (3) and (4) imply τ_{w} → (¬run_{j} atnext β_{2}^{j}). (5) By Lemma 5 (Result Exclusion), we are done. □ The next both lemmas describe the invariants that hold at each iteration of the inner respectively outer loop of wait_{j}. Unfortunately, using temporal logic the invariants of nested loops cannot be proved separately since they mutually depend on each other. Therefore, we combine them to one and verify the correctness of the joint proposition

• at the first entry of each loop,

• at the transition to the next iteration of each loop,

• at the exit of each loop,

• at the entry of a loop when another process is executed. This yields seven cases for both loops (since the exit of the inner loop coincidences with the entry of the outer loop). Lemma 24 (Remove Loop) At the start of each iteration of the inner loop of wait_{j}, j is only in the wait sets W_{i} of all i ∈ Q_{j}:

τ_{w} → (( at{β_{15}^{j}} →

∀i ∈ Q_{j}(elem_{i}(j, W_{i}))∧
∀i ∈ \overline{R}_{j}\Q_{j}(¬elem_{i}(j, W_{i}))) until τ_{r}).

Proof: The proof is contained in the proof of Lemma 25 (Wait Loop). □ Lemma 25 (Wait Loop) At the start of each iteration of the outer loop of wait_{j}, the following invariant holds:

1. If found_{j} then j is not in any wait set W_{i}.

2. If ¬found_{j} then j is only in the wait sets W_{i} of all i ∈ \overline{R}_{j}\P_{j}. Formally,

τ_{w} → (( at{β_{3}^{j}} →

(found_{j} ∧ ∀i ∈ \overline{R}_{j}(¬elem_{i}(j, W_{i}))) ∨
(¬found_{j} ∧ ∀i ∈ P_{j}(¬elem_{i}(j, W_{i})) ∧ ∀i ∈ \overline{R}_{j}\P_{j}(elem_{i}(j, W_{i}))) until τ_{r}).

Proof: We will prove this lemma simultaneously with Lemma 24 (Remove Loop). Define (1) E ≡ found_{j} ∧ ∀i ∈ \overline{R}_{j}(¬elem_{i}(j, W_{i}))

(2) F ≡ ¬found_{j} ∧ ∀i ∈ P_{j}(¬elem_{i}(j, W_{i})) ∧ ∀i ∈ \overline{R}_{j}\P_{j}(elem_{i}(j, W_{i}))

(3) G ≡ ∀i ∈ Q_{j}(elem_{i}(j, W_{i})) ∧ ∀i ∈ \overline{R}_{j}\Q_{j}(¬elem_{i}(j, W_{i})) H ≡ ( at{β_{3}^{j}} → (E ∨ F)) ∧ ( at{β_{15}^{j}} → G) (4) We will prove τ_{w} → (H until τ_{r}). (5) First we have to prove τ_{w} → H (6) which is obviously true. Second let τ be arbitrary fixed with τ_{w} < τ < τ_{r} and assume τ_{w} → (H until τ). (7) We have to prove τ → H. (8) We may restrict our consideration to the following cases τ → △(β_{2}^{j} ∨ ( at{β_{3}^{j}} ∧ ¬β_{3}^{j}) ∨ β_{9}^{j} ∨ β_{14}^{j}) ∨ (9) τ → △(( at{β_{15}^{j}} ∧ ¬β_{15}^{j}) ∨ (β_{15}^{j} ∧ Q_{j} = ∅) ∨ β_{20}^{j}) (10) since otherwise τ → ¬ at{β_{3}^{j}, β_{15}^{j}}.

Case τ → △βj2 By the case assumption, we know τ → at{β_{3}^{j}}. (11) By Lemma 19 (Entry) and Lemma 1 (Locality), we know τ → (¬found_{j} ∧ P_{j} = \overline{R}_{j} ∧ ∀i ∈ \overline{R}_{j}(¬elem_{i}(j, W_{i}))) (12) and thus τ → F. (13)

Case τ → △( at{βj3} ∧ ¬βj3) By the case assumption, we know τ → at{β_{3}^{j}}. (14) By the induction hypothesis (7), we also know τ → △(E ∨ F). (15) By Lemma 1 (Locality) and Lemma 5 (Result Exclusion), we then know τ → E ∨ F. (16)

Case τ → △βj9 By the case assumption, we know τ → at{β_{3}^{j}}. (17) By the induction hypothesis (7) and Axiom 14 (While Loop), we know τ → ((H ∧ P_{j} ≠ ∅ ∧ ¬found_{j}) atprev β_{3}^{j}) (18) which implies τ → ((F ∧ P_{j} ≠ ∅) atprev β_{3}^{j}). (19) By the case assumption, Lemma 5 (Result Exclusion) and Lemma 8 (Constancy), we then can derive with the program structure τ → F. (20)

Case τ → △β{j \atop 14}

By the case assumption, we know τ → at{β_{15}^{j}}. (21) By the induction hypothesis (7) and Axiom 14 (While Loop), we know τ → ((F ∧ P_{j} ≠ ∅) atprev β_{3}^{j}). (22) By Lemma 1 (Locality) and Lemma 5 (Result Exclusion), we can derive τ → G. (23)

Case τ → △( at\{β{j \atop 15}\} ∧ ¬β{j \atop 15})

By the case assumption, we know τ → at{β_{15}^{j}}. (24) By the induction hypothesis (7), we know τ → △G. (25) By Lemma 1 (Locality) and Lemma 5 (Result Exclusion), we then know (8).

Case τ → △(β{j \atop 15} ∧ Qj = ∅)

By the case assumption, we know τ → at{β_{3}^{j}}. (26)

By the program structure and Lemma 1 (Locality), we know τ → found_{j}. (27) By the induction hypothesis (7), we know τ → △G. (28) Lemma 5 (Result Exclusion) therefore implies τ → E. (29)

Case τ → △β{j \atop 20}

By the case assumption, we know τ → at{β_{15}^{j}}. (30) By the induction hypothesis (7) and Axiom 14 (While Loop), we know τ → ((G ∧ Q_{j} ≠ ∅) atprev β_{5}^{j}). (31) By Lemma 6 (Set Update) and Lemma 5 (Result Exclusion), we can then derive τ → G. □ (32)

The following lemma describes the state of Π when the outer loop is left i.e. immediately before the critical region is left. Lemma 26 (Wait End) At the end of the main loop of wait_{j}, the process j has either found a result or it is going to be blocked:

τ_{e} →

¬run_{j} ∧
(found_{j} → (∀i(¬elem_{i}(j, W_{i})) ∧ r_{j} ∈ \overline{R}_{j} ∧ y_{r} = \overline{x}_{r_{j}})) ∧
(¬found_{j} → (∀i ∈ \overline{R}_{j}(elem_{i}(j, W_{i})) ∧ ∀i ∉ \overline{R}_{j}(¬elem_{i}(j, W_{i}))))).

Proof: This is a corollary of Lemma 23 (Not Run), Lemma 25 (Wait Loop) and Lemma 5 (Result Exclusion). □ The following two lemmas describe the invariants of the nested loops of result_{i} and are simultaneously proved similar to the previous invariants. Of particular interest is the invariant of the outer loop which not only describes the state at the entry of the loop but more generally the state of Π when the critical region protected by rsem_{j} is entered (which happens at the end of each iteration of the outer loop). Therefore we have to check all exits of this critical region in any process. Lemma 27 (Erase Loop) At the start of each iteration of the inner loop of result_{i}, w_{i} is exactly in the wait sets W_{i′} of all i′ ∈ S_{i}:

τ_{w} → ∀i((( at{α_{13}^{i}} ∧ w_{i} = j) →

(∀i′ ∈ S_{i}(elem_{i′}(w_{i}, W_{i′})) ∧ ∀i′ ∈ R_{w_{i}}\S_{i}(¬elem_{i′}(w_{i}, W_{i′})))) until τ_{r}).

Proof: The proof is contained in the proof of Lemma 28 (Result Loop). □ Lemma 28 (Result Loop) If process j is a member of some wait set W_{i} and no process is in the critical region protected by rsem_{j}, then j is actually a member of all wait sets W_{i} with i ∈ \overline{R}_{j} and j is (at the point of being) blocked:

τ_{w} → (((rsem_{j} ∧ ∃i(elem_{i}(j, W_{i}))) →

(¬found_{j} ∧ ¬run_{j} ∧ ∀i ∈ \overline{R}_{j}(elem_{i}(j, W_{i})) ∧ at\{β_{22}^{j}, β_{24}^{j}\})) until τ_{r}).

Proof: We prove this lemma simultaneously with Lemma 27 (Erase Loop). Let i be arbitrary fixed and define

(1) X_{0} ≡ rsem_{j} ∧ ∃i′(elem_{i′}(j, W_{i′})),

(2) X_{1} ≡ ¬found_{j} ∧ ¬run_{j} ∧ ∀i′ ∈ \overline{R}_{j}(elem_{i′}(j, W_{i′})) ∧ at\{β_{21}^{j}, β_{22}^{j}\}, Y_{0} ≡ at{α_{13}^{i}} ∧ w_{i} = j, (3)

(4) Y_{1} ≡ ∀i′ ∈ S_{i}(elem_{i′}(w_{i}, W_{i′})) ∧ ∀i′ ∈ R_{w_{i}}\S_{i}(¬elem_{i′}(w_{i}, W_{i′})). We want to prove τ_{w} → ((X_{0} → X_{1}) ∧ (Y_{0} → Y_{1})) until τ_{r}. (5) We know by Lemma 19 (Entry) τ_{w} → (¬X_{0} ∧ ¬Y_{0}) (6) Let time τ be arbitrary fixed with τ_{w} < τ < τ_{r} and assume τ_{w} → (((X_{0} → X_{1}) ∧ (Y_{0} → Y_{1})) until τ). (7) We have to prove τ → ((X_{0} → X_{1}) ∧ (Y_{0} → Y_{1})). (8) We may restrict our considerations to the following cases:

1. τ → △β{j \atop 21}: the critical region protected by rsem_{j} is left and X_{0} may become true.

2. τ → △(β{j \atop 22} ∨ β{j \atop 24}): at\{β_{22}^{j}, β_{24}^{j}\} may become false.

3. τ → △(wi = j ∧ (α{i \atop 12} ∨ at\{α{i \atop 13}\} ∨ α{i \atop 18})): Y_{0} becomes true.

4. τ → △(α{i′ \atop 22} ∧ wi_{′} = j): the critical region protected by rsem_{j} is left and X_{0} may

become true. For all other actions, obviously either

• τ → ¬X_{0} ∧ ¬Y_{0} i.e. the premises are false or

• τ → (△X_{1} → X_{1}) and τ → (△Y_{1} → Y_{1}) i.e. the conclusions are not changed.

Case τ → △β{j \atop 21}

We assume τ → X_{0}. (9) We then know by the case assumption and Lemma 26 (Wait End) τ → △(¬run_{j} ∧ found_{j} ∧ ∀i ∈ \overline{R}_{j}(elem_{i}(j, W_{i}))) (10) and thus by the program structure also τ → (¬run_{j} ∧ found_{j} ∧ ∀i ∈ \overline{R}_{j}(elem_{i}(j, W_{i})) ∧ at\{β_{22}^{j}\}). (11) Therefore, we know τ → X_{1}. (12) By Lemma 5 (Result Exclusion), we also know τ → ¬Y_{0}. (13)

Case τ → △β{j \atop 22}

We assume τ → X_{0}. (14) The case assumption then implies τ → △X_{0} (15) and thus by the induction hypothesis (7) τ → △X_{1}. (16) This implies τ → △¬found_{j} (17) and thus by Axiom 13 (One Branch Conditional) τ → at{β_{24}^{j}}. (18) From this and (16), we know τ → X_{1}. (19) If we assume τ → Y_{0} (20) we also know by the program structure τ → △Y_{0} (21) and thus by the induction hypothesis (7) and the program structure τ → Y_{1}. (22)

Case τ → △β{j \atop 24}

The case assumption implies by Axiom 11 (Wait Statement) τ → △run_{j}. (23) Then we know by the induction hypothesis (7) τ → △¬X_{0} (24) and by the program structure also τ → ¬X_{0}. (25) Let us assume τ → Y_{0}. (26) Then we know by the case assumption τ → △Y_{0} (27) and thus by the induction hypothesis (7) and the program structure τ → Y_{1}. (28)

Case τ → △(α{i \atop 12} ∧ wi = j) By Axiom 11 (Wait Statement) and Lemma 22 (Lock), we know τ → ((rsem_{j} ∧ elem_{i}(j, W_{i})) atprev α_{7}^{i}). (29) By the induction hypothesis (7), we thus know τ → (X_{0} atprev α_{7}^{i}). (30)

By the program structure, Lemma 5 (Result Exclusion) and Lemma 2 (Wait Semaphore), we then know τ → ∀i′ ∈ \overline{R}_{j}(elem_{i′}(j, W_{i′})) (31) and thus also τ → Y_{1}. (32) By Lemma 5 (Result Exclusion), we also know τ → ¬X_{0}. (33)

Case τ → △( at\{α{i \atop 13}\} ∧ wi = j) By the induction hypothesis (7) we have τ → △Y_{1} (34) and thus by Lemma 5 (Result Exclusion) τ → Y_{1}. (35) By Lemma 5 (Result Exclusion), we also know τ → ¬X. (36)

Case τ → △(α{i \atop 18} ∧ wi = j) By the induction hypothesis (7) and Axiom 14 (While Loop), we know τ → ((Y_{1} ∧ S_{i} ≠ ∅) atprev α_{13}^{i}). (37) ant then by Lemma 5 (Result Exclusion) and Lemma 2 (Wait Semaphore) τ → (∀i′ ∈ S_{i}(elem_{i′}(j, W_{i′})) ∧ ∀i′ ∈ \overline{R}_{j}\S_{i}(¬elem_{i′}(j, W_{i′}))). (38) By Lemma 5 (Result Exclusion), we then have τ → Y_{1}. (39) By Lemma 5 (Result Exclusion), we also know τ → ¬X_{0}. (40)

Case τ → △(α{i′ \atop 23} ∧ wi_{′} = j) We know by Lemma 5 (Result Exclusion) τ → ¬Y_{0}. (41) We know by Axiom 11 (Wait Statement) τ → (rsem_{j} atprev α_{7}^{i′})). (42) We will now distinguish two cases:

1. Case τ → (j ∈ Wi_{′} atprev α{i′ \atop 7}) We will show τ → ¬X_{0} (43) by proving τ → ∀k(¬elem_{k}(j, W_{k})). (44) By the induction hypothesis (7), we know τ → ((elem_{i′}(j, W_{i′}) ∧ ∀k ∈ R_{j}(elem_{k}(j, W_{k}))) atprev α_{7}^{i′}). (45)

Then we also have, by Lemma 5 (Result Exclusion), τ → (j ∈ W_{i′} atprev α_{9}^{i′}). (46) From this and the program structure, we then know τ → ((^{◯} at{α_{12}^{i′}}) atprev α_{11}^{i′}). (47) Furthermore, by the induction hypothesis (7) we know τ → (∀k(¬elem_{k}(j, W_{k})) atprev α_{19}^{i′}) (48) which leads by Lemma 5 (Result Exclusion) to (44).

2. Case τ → (j ∉ Wi_{′} atprev α{i′ \atop 7}) We assume τ → X_{0}. (49) By Lemma 5 (Result Exclusion), we know τ → (w_{i′} ∉ W_{i′} atprev α_{9}^{i′}) (50) and thus by Axiom 13 (One Branch Conditional) τ → ((^{◯} at{α_{22}^{i′}}) atprev α_{11}^{i′}) (51) From this we know by (49) and Lemma 5 (Result Exclusion) τ → (X_{0} atprev α_{7}^{i′}). (52) From the induction hypothesis (7), we thus know τ → (X_{1} atprev α_{7}^{i′}) (53) Then we have by (50), (51) and Lemma 5 (Result Exclusion) τ → X_{1}. □ (54)

The final case distinction in the previous proof actually describes an interesting situation. It may happen that some Π_{i} with i ∈ R_{j} finds at α_{5} that j ∈ W_{i} but has to detect at α_{9} that j ∉ W_{i}! In this case, some other Π_{i′} with i′ ∈ R_{j} has executed α_{5} simultaneously to Π_{i} but was slightly faster in executing α_{7}. It “stole” therefore j from W_{i} and delivered x_{i′} to j. The lock of rsem_{j} at α_{7} is therefore necessary to determine a unique winner of the “race”. Lemma 29 (Result End) If process i is going to awake process j, j is not in any wait set W_{i′} any more:

τ_{w} → □∀i((α_{21}^{i} ∧ w_{i} = j) → ∀i′(¬elem_{i′}(j, W_{i′}))) Proof: Let i be arbitrary fixed and let τ > τ_{w} such that τ → (α_{21}^{i} ∧ w_{i} = j). (1) By the program structure, we then know τ → (S_{i} = ∅ atprev α_{13}^{i}). (2) By Lemma 27 (Erase Loop), this implies τ → (∀i′(¬elem_{i′}(j, W_{i′}) atprev α_{13}^{i}). (3) By Lemma 5 (Result Exclusion), we therefore know τ → ∀i′(¬elem_{i′}(j, W_{i′})). □ (4)

The last lemma in this subsection describes the state of Π immediately before wait_{j} is left. This lemma is necessary for two purposes:

1. To guarantee that Lemma 19 (Entry) holds for the next execution of wait_{j}.

2. To guarantee that, after some Π_{i} has set the values of r_{j} and y_{j}, they are not changed

any more by any Π_{i′}. Lemma 30 (Exit) When wait_{j} is left, found_{j} and run_{j} are false and j is not in any wait set W_{i} and no process i is going to deliver its result to j:

t_{f} → ((¬found_{j} ∧ ¬run_{j} ∧ ∀i(¬elem_{i}(j, W_{i}) ∧ ( at{α_{1}2^{i} … α_{21}^{i}} → w_{i} ≠ j)))

   until τ_{r})

Proof: By Lemma 23 (Not Run), we know τ_{e} → ¬run_{j}. (1) We will now distinguish two cases.

1. Case τe → foundj By the program structure and Lemma 1 (Locality), we know τ_{e} → ((¬found_{j}) until τ_{r}). (2) By Lemma 4 (Result Semaphore), we know τ_{e} → ∀i( at{α_{8}^{i} … α_{22}^{i}} → w_{i} ≠ j). (3) By (1), Lemma 26 (Wait End) and the program structure, we know τ_{e} → (∀i(¬elem_{i}(j, W_{i})) until τ_{r}) (4) and with (3) therefore τ_{e} → (∀i((α_{9}^{i} ∧ w_{i} = j) → (w_{i} ∉ W_{j})) until τ_{r}) (5) By (1) and the program structure, it is then easy to derive τ_{e} → (B upto τ_{r}). (6)

2. Case τe → ¬foundj By the program structure, we know τ_{e} → (β_{24}^{j} before τ_{r}). (7) Define τ_{g} with τ_{e} < τ_{g} < τ_{r} such that τ_{e} → (τ_{g} atnext β_{24}^{j}). (8) By Axiom 11 (Wait Statement), we know τ_{g} → run_{j}. (9) By (1) this implies for some i τ_{e} → ((α_{21}^{i} ∧ w_{i} = j) before τ_{g}). (10) Therefore, we know by the program structure and Lemma 29 (Result End) τ_{e} → (∀i(¬elem_{i}(j, W_{i})) before τ_{g}). (11) From this and the definition of α_{21}^{i}, we can derive τ_{f} → (B upto τ_{r}) (12) and are done. □

B.5 Continuation Lemmas

In the section, we deal with all lemmas expressing eventuality properties. In our case, these are assertions that

1. Critical regions protected by a semaphore are left.

2. While loops terminate. The organization of proofs is as follows:

1. Wait Continuation: Lemma 31 says that the critical regions protected by wsem_{i} are left. These regions do not contain other critical regions or while loops.

2. Remove Induction: Lemma 32 says that the inner loop of wait_{j} (which only contains wsem_{i} regions) terminates.

3. Wait Induction: Lemma 33 says that the outer loop of wait_{j} (which contains the wsem_{i} region and an inner loop) terminates.

4. Erase Induction: Lemma 34 says that the inner loop of result_{i} (which contains a critical region protected by wsem_{i}) terminates.

5. Result Continuation: Lemma 35 says that the critical regions protected by rsem_{j} are left. These regions contain the outer loop of wait_{j} and the inner loop of result_{i}.

6. Result Induction: Lemma 38 shows that the outer loop of result_{i} (which contains critical regions protected by rsem_{j} and wsem_{i} and an inner loop) terminates.

7. First Out: Lemma 39 provides an alternative condition that is sufficient to prove

Theorem 5 (Sometimes). Lemma 31 (Wait Continuation) No critical region protected by some wsem_{i} will be occupied forever:

τ_{Π} → □∀i(◇wsem_{i}). Proof: Let time τ ≥ τ_{Π} and i be arbitrary fixed and assume τ → ¬wsem_{i}. (1) By Lemma 2 (Wait Semaphore), we then know τ → at{α_{4}^{i} … α_{6}^{i}, α_{9}^{i}, α_{10}^{i}, α_{24}^{i}} ∨ (2) τ → ∃i′(s_{i′} = i ∧ at{α_{16}^{i′}, α_{17}^{i′}}) ∨ (3) τ → ∃j(p_{j} = i ∧ at{β_{6}^{j} … β_{8}^{j}, β_{10}^{j}}) ∨ (4) τ → ∃j(q_{j} = i ∧ at{β_{18}^{j}, β_{19}^{j}}). (5) All of the denoted regions are terminated by V(wsem_{i}) and no one contains an endwhile or a P statement. Hence, we know by Axiom 16 (Fairness) τ → ◇wsem_{i}. □ (6)

Lemma 32 (Remove Induction) The inner loop in wait_{j} terminates:

τ_{Π} → □(β_{15}^{j} → ◇(β_{15}^{j} ∧ Q_{j} = ∅)). Proof: This can be easily verified by induction over Q_{j} i.e. by proving the assertion

τ_{Π} → □∀\overline{Q}(

(β_{15}^{j} ∧ Q_{j} = \overline{Q} ∧ \overline{Q} ≠ ∅) →
((^{◯}◇β_{15}^{j}) ∧ (Q_{j} ⊂ \overline{Q} atnext β_{15}^{j})))

by the application of Lemma 31 (Wait Continuation) and Axiom 16 (Fairness). □

Lemma 33 (Wait Induction) The outer loop in wait_{j} terminates:

τ_{Π} → □(β_{3}^{j} → ◇(β_{3}^{j} ∧ (P_{j} = ∅ ∨ found_{j})). Proof: We will prove this by induction over P_{j} i.e. by proving the assertion

τ_{Π} → □∀\overline{P} (

(β_{3}^{j} ∧ P_{j} = \overline{P} ∧ \overline{P} ≠ ∅ ∧ ¬found_{j}) →
((^{◯}◇β_{3}^{j}) ∧ ((found_{j} ∨ P_{j} ⊂ \overline{P}) atnext β_{3}^{j}))).

Let time τ > τ_{Π} and \overline{P} be arbitrary fixed such that τ → (β_{3}^{j} ∧ P_{j} = \overline{P} ∧ \overline{P} ≠ ∅). (1) By Axiom 16 (Fairness), it is clear that τ → ^{◯}◇β_{6}^{j}. (2) We will distinguish two cases:

1. Case τ → (¬availpj atnext βj6)) By Lemma 31 (Wait Continuation) and Lemma 16 (Fairness), we know τ → ^{◯}◇β_{3}^{j}. (3) Furthermore, we can easily show τ → (P_{j} ⊂ \overline{P} atnext β_{3}^{j}). (4)

2. Case τ → (availpj atnext βj5)) By Lemma 32 (Remove Induction), we can prove τ → ^{◯}◇β_{3}^{j}. (5) Furthermore, by the program structure it is easy to show τ → (found_{j} atnext β_{3}^{j}). □ (6)

Lemma 34 (Erase Induction) The inner loop in result_{i} terminates:

τ_{Π} → □∀i(α_{13}^{i} → ◇(α_{13}^{i} ∧ S_{i} = ∅)). Proof: This can be easily verified by induction over S_{i} i.e. by proving the assertion

τ_{Π} → □∀i∀\overline{S}(

(α_{16}^{i} ∧ S_{i} = \overline{S} ∧ \overline{S} ≠ ∅) →
((^{◯}◇α_{16}^{i}) ∧ (S_{i} ⊂ \overline{S} atnext α_{16}^{i})))

by the application of Lemma 31 (Wait Continuation) and Axiom 16 (Fairness). □ Lemma 35 (Result Continuation) No critical region protected by some rsem_{j} will be occupied forever:

τ_{Π} → □◇rsem_{j}. Proof: Let time τ ≥ τ_{Π} be arbitrary fixed such that τ → ¬rsem_{j}. (1) We will prove τ → ◇rsem_{j}. (2) By Lemma 4 (Result Semaphore), we have one the following cases:

1. Case τ → at\{βj3 … β{j \atop 21}\}

By Lemma 33 (Wait Induction), we can prove

τ → ◇(β_{3}^{j} ∧ (P_{j} = ∅ ∨ found_{j})). (3)

By Axiom 16 (Fairness), we then know

τ → ◇β_{20}^{j} (4)

and are done.

2. Case τ → (wi = j ∧ at\{αi8 … α{i \atop 22}\}) By Lemma 31 (Wait Continuation), we know τ → ◇α_{9}^{i}. (5) We may assume τ → (j ∈ W_{i} atnext α_{9}^{i}) (6) since otherwise Axiom 13 (One Branch Conditional) and Axiom 16 (Fairness) would directly lead to (8). Then we know by the program structure and Lemma 34 (Erase Induction) τ → ◇(α_{13}^{i} ∧ S_{i} = ∅) (7) which leads to τ → ◇α_{22}^{i}. □ (8)

The following lemma says that result_{j} puts j only in such W_{i} where the corresponding Π_{i} has not yet terminated. Lemma 36 (Terminate) If process j has put the identifier j into some wait set W_{i}, then the process i has not yet terminated:

τ_{w} → (( at\{β_{3}^{j}\} ∧ ¬found_{j}) → ∀i ∈ \overline{R}_{j}\P_{j}(¬ at\{α_{24}^{i}, α_{e}^{i}\})) until τ_{r}. Proof: Define D ≡ ∀i ∈ \overline{R}_{j}\P_{j}(¬ at\{α_{24}^{j}, α_{e}^{j}\})). (1) By the definition of τ_{w}, we know τ_{w} → ¬ at{β_{3}^{j}}. (2) Let time τ be arbitrary fixed with τ_{w} < τ < τ_{r} and assume τ → ( at{β_{3}^{j}} ∧ ¬found_{j}). (3) We are going to prove τ → D. (4) We know by the program structure τ → △(( at{β_{3}^{j}} ∧ ¬β_{3}^{j}) ∨ β_{2}^{j} ∨ β_{9}^{j} ∨ β_{15}^{j}) (5) and may therefore restrict our considerations to the following cases.

Case τ → △( at{βj3} ∧ ¬βj3) By the induction hypothesis, we know τ → △∀i ∈ \overline{R}_{j}\P_{j}(¬ at\{α_{23}^{i}, α_{e}^{i}\}). (6) By (3) and Lemma 25 (Wait Loop), we also know τ → △∀i ∈ \overline{R}_{j}\P_{j}(elem_{i}(j, P_{i})). (7) and therefore τ → △∀i ∈ \overline{R}_{j}(α_{4}^{i} → W_{i} ≠ ∅) (8) and are thus done.

Case τ → △βj2 By the program structure and Lemma 1 (Locality), we know τ → P_{j} = \overline{R}_{j} (9) and are therefore done.

Case τ → △β{j \atop 15}

By the program structure and Lemma 14 (Found), we know τ → found_{j} (10) and are therefore done.

Case τ → △βj9 Let i be arbitrary fixed such that τ → i ∈ \overline{R}_{j}\P_{j}. (11) Let time τ_{1} > τ_{w} such that τ → (τ_{1} atprev β_{3}^{j}). (12) We will distinguish two cases:

1. Case τ_{1} → i ∈ \overline{R}_{j}\P_{j} By the induction hypothesis, we know τ_{1} → ¬ at{α_{24}^{i}, α_{e}^{i}}. (13) Lemma 25 (Wait Loop) and (3) imply τ_{1} → elem_{i}(j, W_{i}) (14) By Lemma 4 (Result Semaphore), we also know τ_{1} → (¬rsem_{j} until τ) (15) and thus by Lemma 5 (Result Exclusion) τ_{1} → (elem_{i}(j, W_{i}) until τ). (16) But then we also know τ_{1} → ((α_{4}^{i} → W_{i} ≠ ∅) until τ) (17) and are therefore done.

2. Case τ_{1} → i ∈ P_{j} Let time τ_{2} such that τ → (τ_{2} atprev β_{6}^{j}). (18) We know by the case assumption and Axiom 12 (Two Branch Conditional) τ_{2} → (p_{j} = i ∧ ¬avail_{i}) (19) and therefore by Lemma 9 (Available) τ_{2} → ¬ at{α_{3}^{i} … α_{e}^{i}}. (20)

Let τ_{3} such that

τ_{2} → (τ_{3} atnext β_{8}^{j}). (21)

From Lemma 2 (Wait Semaphore) and (20), we can conclude

τ_{3} → ¬ at{α_{4}^{i} … α_{e}^{i}}. (22)

Furthermore, we know by the program structure and Lemma 5 (Result Exclusion) τ_{3} → elem_{i}(j, W_{i}). (23) From both assertions we can conclude τ_{3} → ((α_{4}^{i} → j ∈ W_{i}) until τ) (24) and therefore τ_{3} → (¬ at{α_{24}^{i}, α_{e}^{i}} until τ). □ (25)

Lemma 37 (Iteration) If j is in W_{i} outside the critical region protected by rsem_{j}, then eventually a new iteration of the outer loop of result_{j} will start.

τ_{w} → (∀i((rsem_{j} ∧ elem_{i}(j, W_{i})) → ◇α_{4}^{i} until τ_{r}). Proof: Let τ with τ_{r} ≤ τ < τ_{w} and i be arbitrary fixed such that τ → rsem_{j} ∧ elem_{i}(j, W_{i}). (1) By Lemma 21 (Waiting), we know τ_{w} → (β_{21}^{j} before τ). (2) By the program structure, there exists a time τ′ with τ_{w} < τ′ < τ such that τ′ → (β_{3}^{j} ∧ ¬found_{j} ∧ P_{j} = ∅). (3) By Lemma 36 (Terminate) and Lemma 20 (Membership), we then know τ′ → ¬ at{α_{24}^{i}, α_{e}^{i}} (4) i.e. we know by Lemma 27 (Erase Loop) and Lemma 35 (Result Continuation) τ′ → ◇α_{4}^{i} (5) and are done. □ The following lemma shows that not only wait_{j} but also result_{i} terminates. This is the main constituent in the proof of Theorem 5 (Sometime). Lemma 38 (Result Induction) The outer loop in result_{i} terminates:

τ_{w} → ∀i((rsem_{j} ∧ elem_{i}(j, W_{i})) → ◇(α_{4}^{i} ∧ W_{i} = ∅)) until τ_{r}. Proof: Let τ with τ_{w} < τ < τ_{r} and i be arbitrary fixed such that τ → (rsem_{j} ∧ elem_{i}(j, W_{i})). (1) By Lemma 37 (Iteration), we know τ → ◇α_{4}^{i}. (2) Let us assume that for some \overline{W} ≠ ∅ τ′ → W_{i} = \overline{W} . (3) It now suffices to show τ′ → (W_{i} ⊂ \overline{W} atnext α_{4}^{i}). (4) By Lemma 9 (Available), we know τ′ → □avail_{i}. (5)

This implies by Lemma 2 (Wait Semaphore) τ′ → □∀j(β_{7}^{j} → p_{j} ≠ i) (6) i.e. W_{i} will be not extended any more by any other process. Define j such that τ′ → (w_{i} = j atnext α_{6}^{i}). (7) We know by Lemma 2 (Wait Semaphore) τ′ → j ∈ W_{i}. (8) In case of τ′ → (j ∉ W_{i} atnext α_{9}^{i}) (9) we are done. Otherwise, Lemma 29 (Result End) implies τ′ → (j ∉ W_{i} atnext α_{21}^{i}) (10) and we are done. □ The following lemma can be proved using the additional Axiom 18 (Queue) and may be used in an alternative proof of Theorem 5 (Sometime) in case that (by a modification in the program structure) Lemma 38 (Result Induction) does not hold: Lemma 39 (First Out) No j will remain in W_{i} forever:

τ_{w} → ∀i((rsem_{j} ∧ elem_{i}(j, W_{i})) → ◇(¬elem_{i}(j, W_{i}))) until τ_{r}. Proof: Let τ with τ_{w} < τ < τ_{r} and i be arbitrary fixed such that τ → (rsem_{j} ∧ elem_{i}(j, W_{i})). (1) By Lemma 37 (Iteration), we know that for some time τ′ > τ τ′ → α_{4}^{i}. (2) We may assume τ′ → elem_{i}(j, W_{i}) (3) since otherwise we are done. By Lemma 35 (Result Continuation) and Lemma 27 (Erase Loop), we know τ′ → □(α_{4}^{i} → (W_{i} = ∅ ∨^{◯}◇α_{4}^{i})) (4) i.e. the iteration will continue forever unless W_{i} becomes empty. We may assume τ′ → □(α_{4}^{i} → ^{◯}◇α_{4}^{i}) (5) since otherwise we are done (see Lemma 38 (Result Induction)). By the program structure and Lemma 27 (Erase Loop), we know for some j′ τ′ → ^{◯}((j′ = w_{i} ∧ w_{i} ∉ W_{i}) atnext α_{4}^{i}). (6) We may assume j ≠ j′ since otherwise we are done. But, by Axiom 18 (Queue), we know τ′ → j′ ∈ W_{i}. (7) Since there are only finitely many such j′, we know with (5) τ′ → ◇w_{i} = j (8) and are therefore done. □

C The Program Model

resulti(x_{i}) ≡

(α_{1}^{i}) value_{i} := x_{i} (α_{2}^{i}) avail_{i} := true

(α_{3}^{i}) P(wsem_{i}) (α_{4}^{i}) while W_{i} ≠ ∅ do (α_{5}^{i}) w_{i} ∈ W_{i} (α_{6}^{i}) V(wsem_{i})

(α_{7}^{i}) P(rsem_{w_{i}})

(α_{8}^{i}) P(wsem_{i}) (α_{9}^{i}) deliver_{i} := w_{i} ∈ W_{i} (α_{10}^{i}) V(wsem_{i})

(α_{11}^{i}) if deliver_{i} then

(α_{12}^{i}) S_{i} := R_{w_{i}} (α_{13}^{i}) while S_{i} ≠ ∅ do (α_{14}^{i}) s_{i} ∈ S_{i} (α_{15}^{i}) P(wsem_{s_{i}}) (α_{16}^{i}) rem(W_{s_{i}}, w_{i}) (α_{17}^{i}) V(wsem_{s_{i}}) (α_{18}^{i}) S_{i} := S_{i}\{s_{i}}

endwhile

(α_{19}^{i}) y_{w_{i}} := x_{i} (α_{20}^{i}) r_{w_{i}} := i (α_{21}^{i}) V(run_{w_{i}})

endif

(α_{22}^{i}) V(rsem_{w_{i}})

(α_{23}^{i}) P(wsem_{i})

endwhile (α_{24}^{i}) V(wsem_{i})

(α_{e}^{i}) stop waitj(y_{j}, r_{j}, R_{j}) ≡

(β_{1}^{j}) P_{j} := R_{j}

(β_{2}^{j}) P(rsem_{j}) (β_{3}^{j}) while P_{j} ≠ ∅ ∧ ¬found_{j} do

(β_{4}^{j}) p_{j} ∈ P_{j} (β_{5}^{j}) P(wsem_{p_{j}})

(β_{6}^{j}) if ¬avail_{p_{j}} then

(β_{7}^{j}) add(W_{p_{j}}, j) (β_{8}^{j}) V(wsem_{p_{j}}) (β_{9}^{j}) P_{j} := P_{j}\{p_{j}}

else

(β_{10}^{j}) V(wsem_{p_{j}})

(β_{11}^{j}) y_{j} := value_{p_{j}} (β_{12}^{j}) r_{j} := p_{j} (β_{13}^{j}) found_{j} := true

(β_{14}^{j}) Q_{j} := R_{j}\P_{j} (β_{15}^{j}) while Q_{j} ≠ ∅ do (β_{16}^{j}) q_{j} ∈ Q_{j} (β_{17}^{j}) P(wsem_{q_{j}}) (β_{18}^{j}) rem(W_{q_{j}}, j) (β_{19}^{j}) V(wsem_{q_{j}}) (β_{20}^{j}) Q_{j} := Q_{j}\{q_{j}}

endwhile endif

endwhile (β_{21}^{j}) V(rsem_{j})

(β_{22}^{j}) if found_{j} then (β_{23}^{j}) found_{j} := false

else (β_{24}^{j}) P(run_{j})

endif

(β_{e}^{j}) nop