Multi-threading

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

Syntax

 B ::= true | false

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

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


 Stmt ::= if E then Stmt else Stmt         // Conditional statement
    |  V = E                               // Assignment
    |  print V                             // print


 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 we employ operational semantics rules of the form

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

The above states:

• Schedule Thread_1 for execution

• Execute Thread_1 under value assignment S

  • We will execute one statement at a time

• Execution yields Thread_1’ and value assignmet S’

Recall:

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

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

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


              Thread_1 = [Stmt_1] + Thread_1'        (S,Stmt_1) => S'
(Schedule)  -----------------------------------------------------------------------
             (S, {{ Thread_1,...,Thread_k }}) => (S', {{ Thread_1',...,Thread_k }})

Rule (Drop) simply drops a thread that has been fully executed.

Rule (Schedule) picks an arbitrary thread Thread_1.

Recall that {{...}} refers to a multiset. We execute the first statement in Thread_1 and continue with the remaining statements Thread_1’ and the updated value assignment S’.

Here’s some Go implementation that implements the multi-threaded SIMP evaluation rules.