Problem E. Exclusive Access ≡

Statement

One important problem in concurrent programming is to ensure exclusive access to shared resources by multiple threads. It is also known as Mutual Exclusion protocol. A code that needs to be protected from concurrent execution is called critical section (CS). In order to coordinate access to CS, application threads use a set of shared variables to send information to each other. These shared variables are distinct from all the variables that are used by application code. In practice, mutual exclusion protocol is implemented as two methods — enterCS and exitCS. When application needs to execute some code in CS, it calls enterCS, then executes CS, then calls exitCS.

For theoretical analysis of mutual exclusion protocol one must consider running application as a whole. Each thread of application is represented as an infinite loop that repeatedly performs some work unrelated to CS, which is called non-critical section (NCS), then calls enterCS, then executes CS, then calls exitCS, then the loop repeats. The code inside NCS and CS is not relevant; it is considered to perform no operations related to the protocol and does not modify shared variables used by the protocol.

We consider a system with two concurrently running threads. Threads use a set of shared one-bit variables to implement mutual exclusion protocol. Each variable can store a value of zero or one that can be read or written by a single instruction. Shared variables are initialized to zero. Each thread has a local pointer to the instruction (IP) that it is going to execute next. Execution starts from the top of the code. During each step of execution one of the threads is arbitrarily chosen, it executes one instruction, and then changes its IP to the next instruction to execute. This infinite sequence of steps is called history. A history is called legal if either both threads execute infinitely many steps or just one thread does, while the other thread, having taken a finite number of steps, stops with IP at NCS.

The table below contains several algorithms in pseudo-code that attempt to implement mutual exclusion protocol. In this pseudo-code id is 0 for the first thread and 1 for the second. Variables want[0], want[1], and turn are shared between threads to implement mutual exclusion protocol. Lines marked with "\verb|+|" implement enterCS, lines marked with "\verb|-|" implement exitCS. Lines NCS() and CS() are placeholders for some code that works inside non-critical and critical sections respectively and is not relevant for this problem.

The task is to figure out if the given algorithm satisfies three important properties:

• The algorithm satisfies mutual exclusion if in any legal history CS is not executed concurrently by two threads (that is, there is no step where IP of both threads is at CS).
• The algorithm satisfies deadlock freedom if any legal history has infinitely many executions of CS.
• The algorithm satisfies starvation freedom if in any legal history a thread that executes infinitely many steps has infinitely many executions of CS.

The property of mutual exclusion is trivial. The algorithm that simply loops forever doing nothing will satisfy it. The sample algorithms above all satisfy mutual exclusion, but the first two fail to achieve deadlock freedom. The algorithm 3 (originally created by Gary Peterson) satisfies all three properties.

Input file format

The input file starts with a line with two integer numbers — m₁ and m₂, where m_i is the number of lines of code for i-th thread (2 ≤ m_i ≤ 9). It is followed by m₁ lines with the code for the first thread and m₂ lines with the code for the second thread.

• NCS — non-critical section placeholder. Its single argument is NIP.
• CS — critical section placeholder. Its single argument is NIP.
• SET — write value to the shared variable. It has three arguments v, x, and g, where v is the variable to write (A, B, or C), x is the value to write (0 or 1), and g is NIP.
• TEST — read and test the value of the shared variable. It has three arguments v, g₀, and g₁ where v is the variable to read (A, B, or C), g₀ is NIP if the value of the variable is zero, and g₁ is NIP if the value of the variable is one.

Output file format

Constraints

Sample tests

4 4
1 NCS 2
2 TEST C 3 2
3 CS 4
4 SET C 1 1
1 NCS 2
2 TEST C 2 3
3 CS 4
4 SET C 0 1

YNN

5 5
1 NCS 2
2 SET A 1 3
3 TEST B 4 3
4 CS 5
5 SET A 0 1
1 NCS 2
2 SET B 1 3
3 TEST A 4 3
4 CS 5
5 SET B 0 1

YNN

7 7
1 NCS 2
2 SET A 1 3
3 SET C 1 4
4 TEST B 6 5
5 TEST C 6 4
6 CS 7
7 SET A 0 1
1 NCS 2
2 SET B 1 3
3 SET C 0 4
4 TEST A 6 5
5 TEST C 4 6
6 CS 7
7 SET B 0 1

YYY

5 7
1 NCS 2
2 SET A 1 3
3 TEST B 4 3
4 CS 5
5 SET A 0 1
1 NCS 2
2 SET B 1 3
3 TEST A 6 4
4 SET B 0 5
5 TEST A 2 5
6 CS 7
7 SET B 0 1

YYN

3 3
1 SET A 0 1
2 CS 2
3 NCS 3
1 TEST A 1 1
2 CS 2
3 NCS 3

YNN

2 2
1 CS 2
2 NCS 1
1 NCS 2
2 CS 1

NYY