Overview of Method for Relaxed Memory Models

Regarding a loop behavior, the loop body can be described arbitrarily regarding its in-variant condition to abstract the effect of previous loop iterations. Besides, as concurrent programs are the target of our method, the abstraction must also cover the effect of the other concurrent programs which can see the effect of each iteration. In our case, the effect to other programs corresponds to the write operations inside the loop body. Thus, the effect of write events issued by infinite iterations must be abstracted for other programs appropriately. Besides, the motivation of this method is to provide the first-order for-mula for SMT-based program verification automatically. Thus, the abstraction of infinite iterations is expected to be generated automatically.

1γ₁;

2do{

3 v := [ Y ];

4 [ X ] := ψ(v);

5 hinvi

6}while(φ(v)) ;

7γ2;

1r1 :=[ X ];

2r2 :=[ X ];

3. . .

4rk :=[ X ]

Figure 4-2: Infinite Loop Programs with k reads

Although infinite iterations are allowed to occur, there is an assumption that k loop iterations would be sufficient for program verification if there are k read events issued by other processors. For instance, Figure 4-2 shows the concurrent programs where the loop body writes the value which is calculated from ψ(v) to memory location [X] and there are k read operations accessing to memory location [X] on another program. In program verification on relaxed memory models, the program execution is assumed to be eventually terminated. This means there arei iterations to instantiate the loop body where i≥0. However, as there are onlyk read events to memory location[X] issued by

the programs, the number of write events to memory location [X] is at mostk in which the read events get the values from different write events. Also, according to Figure 4-3, although there arei^th iterations that can occur, at most k iterations would be considered to determine the computation on other programs as there are only k read events.

1γ₁;

2// i t e r a t i o n 0

3v := [ Y ];

4[ X ] := ψ(v);

5assume(φ(v)) ;

6. . .

7// i t e r a t i o n 1

8assume(φ(v)) ;

9v := [ Y ];

10[ X ] := ψ(v);

11. . .

12// i t e r a t i o n k

13assume(φ(v)) ;

14v := [ Y ];

15[ X ] := ψ(v);

16. . .

17// i t e r a t i o n i

18assume(φ(v)) ;

19v := [ Y ];

20[ X ] := ψ( v ) ;

21assume(¬φ(v)) ;

22γ₂

1r1 :=[ X ];

2r2 :=[ X ];

3. . .

4rk :=[ X ]

Figure 4-3: k iteration with k reads

According to the assumption, the infinite iterations for k read events are expected to abstracted as an arbitrary effect of k iterations that satisfies the loop invariant. The following description shows the target abstraction which abstracts the effect of write events fromk+ 1 loop iterations whereinv(v, w_x) is the invariant condition that relies on the value of local variable v and write valuew_x.

1// a r b i t r a r y i t e r a t i o n

2v := *;

3assume(φ(v)∧inv(v, wx)) ;

4// i t e r a t i o n 1

5[ X ] := w_x;

6assume(φ(v)∧inv(v, wx)) ;

7. . .

8// i t e r a t i o n k +1

9[ X ] := wx;

10assume(φ(v)∧inv(v, w_x)) ;

11v := [ Y ];

12[ X ] := ψ(v);

By the assumption, the number of the read events on other programs is the concern to abstract a loop iteration. Besides, iteration (k + 1)^th is used to abstract the prior iteration for the read events in an arbitrary loop iteration. However, if there is a loop on other programs, the number of events could be infinite that also affects the number of abstraction.

Regarding the number of the read events caused by loop behaviors, the infinite number of the read events would be caused by the behavior that waits for the read values from outside not to satisfy the loop condition. In the purpose of program verification, arbitrary behavior of loop body is considered in which the read value can be affected by outside memory events. Thus, the number of the read events to be considered caused by the loop equals the number of the read operations. For instance, the following description is an arbitrary loop iteration ofdo{v := [X];u:= [Y]hinv(v, u)i}while(φ(v, u)).

1// a r b i t r a r y e f f e c t

2v := *;

3u := *;

4assume(φ(v, u)∧inv(v, u)) ;

5// a r b i t r a r y i t e r a t i o n

6v := [ X ];

7u := [ Y ];

If there is a loop on another program to write values to memory locations [X] and [Y], at most two loop iterations can be considered to consider this arbitrary value of this arbitrary loop iteration.

Given concurrent programs P =P₁·Qwhere Q=P₂·. . .·P_n and each P_i is executed on processing unitisuch that 1≤i≤n. LetP₁ be γ₁;do{γ_shinvi}while(c);γ₂ andQbe arbitrary programs that can read and write to the same memory locations that P1 uses.

Thus, the method derives the control flows to be verified regarding the loop invariant in P₁ and the number of read events that access the same memory locations that γ_s access. For simplicity, the control flow graph shown in Figure 4-4 derives the execution of P₁ regarding invariant condition inv where arb v is the arbitrary assignments of local variables and arb wⁱ is the arbitrary assignment of memory locations for iteration i. In

addition, k is the number of read events appearing in Q that access the same memory locations written by the write operations in the loop body.

Figure 4-4: Overview of Inductive Invariant Method

For the arbitrary assignment of local variables arb v, we collect the assigning target of the read operation and load-link operation to the local variables. Those local variables are assigned by arbitrary values for considering the arbitrary effect from the previous iteration. Then, assumption assume(c∧inv) is used to restrict the scope of assigning values to those local variables.

For the arbitrary assignment of memory locations arb w, we consider the target assign-ment of write operations and store-condition operations to the memory locations. Due to the behavior of store-condition operation, there is a possibility the write event issued by the operation can fail. Besides, the sequence of write operations would be the matter because of the behavior of store-condition operations. Thus, the possible ways to issue the write events from the loop body are considered for the arbitrary assignment of memory locations arb w. For instance, the following description illustrates the loop body to be abstracted for arb w.

1// l o o p b o d y

2u := v + z ;

3[ X ] := u ;

4 i f( z = 1) {

5 sc ( z , [ X ] , u ) ;

6 [ X ] := v ;

7}

Figure 4-5 shows the control flow graph by analyzing the possible ways to issue the write events regarding the program order. Note that there are restrictions in this method that

(1) the local variable for assigning the result of store-condition operation must not be used in the read operations and load-link operations, and (2) the loop behavior is not allowed as a nested loop. Then, the arbitrary assignment to memory locations must consider every case to issue the write events.

Figure 4-5: Control flow graph for considering arbitrary assignments to memory locations To summarize, each control flow derived from the graph is then considered regarding the target memory model as the same as the bounded method. In this method, the way to abstract the effect of infinite iterations is the primary concern for program verification on relaxed memory models. This means after the loop behavior is abstracted, the encoding method for program verification using SMT-solver is the same. However, as this method also use the invariant condition to restrict the scope of write values to memory locations, the assertion language is also improved to support such requirement.

Nevertheless, the proposed inductive invariant method did not take the memory events occurring after a loop iteration into account. This means this method would not be sound for any relaxed memory models. However, as partial store ordering (PSO) doesn’t allow a read operation to be delayed; thus, the method is sound for PSO and stronger memory models.