Assignment : Verifying program under sequential consistency

Description

• Background

Initially: x=0

p1 p2

x=1 x=2

r1=x r2=x

Figure 1: A sample program

Concurrent Program: Concurrent program P contains fixed num-ber of processes p₁, p₂, …p_n.. Each process contains write or read in-structions. write instructions are of form x = d, where x is global variable and d is an integer. read instructions are of form r = x, where r is local register and x is global variable.

Sequential Execution An execution is sequence of instructions. An execution is sequential iff all read instructions read values from latest write instructions. For an execution E e₁, e₂, …, e_m, where e_i = {write or read} instruction , in_E(e) denotes the index of in-struction e in the Execution E.

An execution E is sequential iff (i) every read instruction, r = x, reads value of global variable x from the write instruction x = d₁ (this can be initial value, assume that all global variables are ini-tialized with 0 ) where in_E(r = x) < in_E(x = d₁), and (ii) if r = x reads from x = d₁ then for all write instructions x = d₂ we have either in_E(x = d₂) < in_E(x = d₁) or in_E(r = x) < in_E(x = d₂).

• Assignment

Your task will be to develop a tiny software tool that takes program as input and outputs all valid traces.

Input program can have assert statement in it. If there exists a sequential execution(valid trace) that violates the assert statement, then your tool should stop exploring traces and output the result as “Assertion violation” and display this trace.

Extras, Not mandatory: [You can optimize your algorithm by explor-ing only one trace per rf−equivalence class of traces. Two traces τ₁ = (S_I , po₁, rf₁, ws₁) and τ₂ = (S_I , po₂, rf₂, ws₂) are rf−equivalent if po₁ = po₂ and rf₁ = rf₂.]

Example 1 : Consider that program shown in figure 1 is input program. Output for this input program can be:

1. Trace: [x = 1, r1 = x, x = 2, r2 = x] , rf relation:[[x = 1, r1 = x], [x = 2, r2 = x]], co relation:[[x = 2, x = 1]]

2. Trace: [x = 1, r1 = x, x = 2, r2 = x], rf relation:[[x = 1, r1 = x], [x = 2, r2 = x]], co relation:[[x = 1, x = 2]]

3. Trace: [x = 1, x = 2, r1 = x, r2 = x], rf relation:[[x = 2, r1 = x], [x = 2, r2 = x]], co relation:[[x = 1, x = 2]]

4. Trace: [x = 2, x = 1, r1 = x, r2 = x], rf relation:[[x = 1, r1 = x], [x = 1, r2 = x]], co relation:[[x = 2, x = 1]]

You can output traces and rf, ws relations in any order. But, ensure that each trace is valid trace and you do not repeat same trace(having same rf, ws relations).

Example 1 : Consider that program shown in figure 1 is input pro-gram and it has an assert statement, assert(r2 != 1). Then your tool should output following:

Assertion Violation :

Violating Trace: [x = 2, x = 1, r1 = x, r2 = x], rf relation:[[x = 1, r1 = x], [x = 1, r2 = x]], co relation:[[x = 2, x = 1]]

2.1 Input Format:

First line of input is number of processes, n. Then next n lines contain instructions form the each process. Then next line will be integer A. If A is 1 then the next line will contain assert statement.

If A is 0 then there will be no assert statement for the given pro-gram. Assert statement can have logical ’and’, ’or’ operators, e.g. assert(r2 != 1 and r4 != 2).

Input Example 1 : The program given in the figure 1 will be pre-sented in following format:

2

x=1;r1=x;

x=2;r2=x;

0

Input Example 2 : The program given in the figure 1 with the assert statement, assert(r2 != 1) will be presented in following format:

2

x=1;r1=x;

x=2;r2=x;

1

assert(r2 != 1)

Input Example 3 :

4

x=2;y=1;

y=2;z=1;

z=2;x=1;

r1=x;r2=y;r3=z;

1

assert(r1 != 1 or r2 != 1 or r3 != 1)

2.2 Output Format

Output 1 One of the correct outputs for Input example 1.

No. of traces = 4

1-: Trace: [x = 1, r1 = x, x = 2, r2 = x] , rf relation:[[x = 1, r1 =

x], [x = 2, r2 = x]], co relation:[[x = 2, x = 1]]

2-: Trace: [x = 1, r1 = x, x = 2, r2 = x], rf relation:[[x = 1, r1 = x], [x = 2, r2 = x]], co relation:[[x = 1, x = 2]]

3-: Trace: [x = 1, x = 2, r1 = x, r2 = x], rf relation:[[x = 2, r1 = x], [x = 2, r2 = x]], co relation:[[x = 1, x = 2]]

4-: Trace: [x = 2, x = 1, r1 = x, r2 = x], rf relation:[[x = 1, r1 = x], [x = 1, r2 = x]], co relation:[[x = 2, x = 1]]

Output 2 Output for sample input 2.

Error: Assertion Violation

Violating Trace: [x = 2, x = 1, r1 = x, r2 = x], rf relation:[[x = 1, r1 = x], [x = 1, r2 = x]], co relation:[[x = 2, x = 1]]

2.3 Input Constraints

1. 1 ≤ n ≤ 10.

2. Maximum number of instruction per process = 4

3. Fixed global variables: x , y, and z.

4. Maximum number of local registers in the input program= 10

5. Each read instruction can obtain its value from max 4 write instruction. So, if there is read instruction, r = x, then it can obtain value of x from max 4 write instructions on variable x.

6. Initially x=0 , y=0 , z=0. (Global valuables are initialized with zero.)

2.4 Task

Students will develop the tool in python. Students can form group of 2-3 students to complete the assignment. Along with the code, students need to submit a document(pdf file), de-scribing their algorithm and approach followed. If you complete the assignment in group then mention name and roll no. of all members in the document.

Deadline: 18 Feb 2022, 11:00 PM

Submission Format: Students should develop the tool in python language. The driver file(which accepts the input program and out-puts the traces) should be named as trace.py. You can create other files as per your approach(algorithm).

You need to submit the solution to assignment as the zip file, which

contains all python files(including driver file,trace.py) and pdf file(document where you describe your approach and algorithm). Name the zip file as< your − roll − no >.zip (for groups with 2-3 students, mention roll no. of the any member.)

Marks: Working tool: 14 marks, Document(pdf): 6 marks.

6