Multi-threading and locks

We consider an extension of SIMP where there can be multiple threads of execution and locks.

Syntax

 B ::= true | false

 V ::= "x" | ...                  // Variables

 M ::= "l" | ...                  // Locks

 E ::= B | !E | E && E | V


 Stmt ::= if E then Stmt else Stmt         // Conditional statement
    |  V = E                               // Assignment
    |  print V                             // print
    |  lock M                              // Acquire lock M
    |  unlock M                            // Release lock M


 Thread ::= [Stmt_1,...,Stmt_n]

 Threads ::= {{Thread_1, ..., Thread_k}}

A thread is a sequence of statements represented by a list. We therefore omit “;” in Stmt.

There is no go (or fork) statement. We assume that each thread is represented by a statement and use a multiset to maintain the multiple threads of execution.

Semantics

The operational semantics rules for expressions and statements are as before. For details, see here

For the execution of multiple threads with locks we employ operational semantics rules of the form

(S, L, {{ Thread_1,...,Thread_k }}) => (S', L', {{ Thread_1',...,Thread_k }})

S refers to the value assignment:

S ::= [] | [V : B] | S + S

The additional component L, keeps track of the state of each lock.

L ::= [M1 : B1, ... Mn : Bn]

Mi refers to a lock variable and Bi refers to the state of that lock. Bi equals true means that Mi is locked. Otherwise, unlocked. Initially, for all Mi we find Bi equal to false (i.e., are unlocked).

The operational semantics rules for multi-threaded execution with locks are as follows.

(Drop)     (S, L, {{ [], Thread_1,..., Thread_k }}) => (S, L, {{ Thread_1,..., Thread_k }})



              Thread_1 = [Stmt_1] + Thread_1'        (S,Stmt_1) => S'
              Stmt_1 is not a lock/unlock statement
(Schedule)  -----------------------------------------------------------------------
             (S, L, {{ Thread_1,...,Thread_k }}) => (S', L, {{ Thread_1',...,Thread_k }})



              Thread_1 = [lock M] + Thread_1'
              lockup(L,M) equals false
              L' = [M : true] + L
(Lock)      -----------------------------------------------------------------------
             (S, L, {{ Thread_1,...,Thread_k }}) => (S, L', {{ Thread_1',...,Thread_k }})



              Thread_1 = [unlock M] + Thread_1'
              lockup(L,M) equals true
              L' = [M : false] + L
(Unlock)    -----------------------------------------------------------------------
             (S, L, {{ Thread_1,...,Thread_k }}) => (S, L', {{ Thread_1',...,Thread_k }})

Rule (Drop) simply drops a thread that has been fully executed. Rule (Schedule) picks an arbitrary thread Thread_1. Both rules are as before.

Rule (Lock) acquires the lock M, if M is not locked yet. This means that the lock operation is a potentially blocking operation. If a thread attempts to acquire lock M, but M is locked, then the lock M operation in that thread cannot be executed.

Rule (Unlock) releases the lock M, if M is locked yet. In most programming languages (such as Java and C), the unlock M operation is a non-blocking operation. This means that if we attempt to release lock M, but M is not locked, we abort program execution (“panic”). Hence, we impose the following additional operational semantics rule.

              Thread_1 = [unlock M] + Thread_1'
              lockup(L,M) equals false
(Unlock-2) -----------------------------------------------------------------------
             (S, L, {{ Thread_1,...,Thread_k }}) => PANIC

Here’s some Go implementation that implements the above rules.