Overview

• A simple imperative language

• Multi-threading

• Locks

More to come

A simple imperative language

Task 1

Take a look at the implementation and play around with your own examples.

Task 2

Evaluate the following expression using the operational semantics rules.

y && !x

The initial value assignment is [] (empty).

Task 3

Evaluate the following statement using the operational semantics rules.

if x then y:=true else print x; print x; print y

Task 4

Extend SIMP and include further operations. For example, Boolean disjunction, …

Multi-threading

Task 1

Take a look at the implementation and play around with your own examples.

Task 2

Consider the following multi-threaded execution.

([],
{{
   x = false; x = (!x); print(x)   ,
   x = true; if x { y = true } else { z = true }
}}
)
=>
([ x=false],
{{
   x = (!x); print(x)   ,
   x = true; if x { y = true } else { z = true }
}}
)
=>
([ x=true],
{{
   x = (!x); print(x)   ,
   if x { y = true } else { z = true }
}}
)
=>
([ x=false],
{{
   print(x)   ,
   if x { y = true } else { z = true }
}}
)
=>
([ x=false z=true],
{{
   print(x)
}}
)
Output: false
=>
([ x=false z=true],
{{
}}
)

Give an alternative sequence of evaluation steps where in the final value assignment we find that z=false.

Task 3

Consider the following multi-threaded execution where value assignments are omited.

{{
   x = true; if x { print(x) } else { print(y) }; x = y   ,
   x = false; x = (!x); print(x)
}}
=>
{{
   if x { print(x) } else { print(y) }; x = y   ,
   x = false; x = (!x); print(x)
}}
Output: true
=>
{{
   x = y   ,
   x = false; x = (!x); print(x)
}}
=>
{{
   x = y   ,
   x = (!x); print(x)
}}
=>
{{
   x = (!x); print(x)
}}
=>
{{
   print(x)
}}
Output: true
=>

Complete the above evaluation steps with the missing value assignments.

Locks

Task 1

Take a look at the implementation and play around with your own examples.

Task 2

Consider execution of the following example.

func ts3() {

    // lock(m);x = false; print(x); x = !x; print(x);unlock(m)
    t0 := mkThread(lock("m"), assign("x", boolean(false)), print("x"), assign("x", not(variable("x"))), print("x"), unlock("m"))

    // lock(m);x = true; x = !x; print(x); unlock(m)
    t1 := mkThread(lock("m"), assign("x", boolean(true)), assign("x", not(variable("x"))), print("x"), unlock("m"))

    ts := []Thread{}
    ts = append(ts, t0)
    ts = append(ts, t1)

    runThreads(ts)

}

What can possibly happen? Write down possible evaluation steps.

Task 3

Consider execution of the following example.

func ts4() {

    // lock(m1);lock(m2);unlock(m2)unlock(m1)
    t0 := mkThread(lock("m1"), lock("m2"), unlock("m2"), unlock("m1"))

    // lock(m2);lock(m1);unlock(m1)unlock(m2)
    t1 := mkThread(lock("m2"), lock("m1"), unlock("m1"), unlock("m2"))

    ts := []Thread{}
    ts = append(ts, t0)
    ts = append(ts, t1)

    runThreads(ts)

}

What can possibly happen? Write down possible evaluation steps.