3 Thread safety notation

Notation to indicate the thread-safety-ness of a set of functions

Definition : For functions X,Y, X1...Xn, Y1...Ym we write

     X|Y                        if it is permissible for one thread to call X while another thread calls Y.
     X1|X2|...|Xn               if Xi|Xj for all i != j
     (X1,...,Xn)|(Y1,...,Ym)    if Xi|Yj for all i,j
     ||(X1,...,Xn)              if Xi|Xj for all i,j   i.e.   (X1,...,Xn) | (X1,...,Xn)

     X$Y                        if it is NOT permissible for one thread to call X while another thread calls Y.
                                It is sufficient for example that a single thread calls X then Y or vise versa.
                                Alternatively if there are multiple threads involved then a mutex should be used.
                                The mutex ensures that a call to X comes strictly before or after a call to Y 
                                (i.e. the calls are serialised), and that any changes made by one thread are 
                                fully visible to another.
                                
     X1$X2$...$Xn               if Xi$Xj for all i != j
     (X1,...,Xn)$(Y1,...,Ym)    if Xi$Yj for all i,j
     $$(X1,...,Xn)              if Xi$Xj for all i,j   i.e.   (X1,...,Xn) $ (X1,...,Xn)

    1-2:X                       X can be called once or twice
    -1:X                        if X can be called at most once
     1:X                        if X must be called exactly once
      !x                        if x must be called exactly once
    1+:X                        at least one call to X
    0+:X                        X can be called any number of times (the default)
    
    X < Y                       X must be called before Y
                                If multiple threads are involved then memory barriers must be used to ensure
                                that any changes made by the thread calling X become visible to the thread calling
                                Y.
                                
    (X1,...,Xn)<(Y1,...,Ym)     if Xi < Yj for all i,j

In this notation, X can be used in place of (X) - i.e. when a single function appears in brackets, the brackets are not necessary. For example X|(Y1...Ym) means X|Yj for all j.

It is assumed that ||(X1,...,Xn) can be nested within a larger expression, with the understanding that ||(X1,...,Xn) is equivalent to (X1,...,Xn) in the context of the surrounding expression.

Similarly $$(X1,...,Xn) is equivalent to (X1,...,Xn) when it appears inside a larger expression.

X$Y and X|Y are interpreted as (X,Y) within the context of the containing expression.

Laws

    x $ y = y $ x
    x | y = y | x
    
    x $ x = $$(x)
    x | x = ||(x)

    $$(x,y)  <=>  $$(y,x)
    $$(x,y)   =>  $$(x)

    ||(x,y)  <=>  ||(y,x)
    ||(x,y)   =>  ||(x)
    
    x  x  x   x   not(x  e

    not x$y  <=>  x|y
    not x|y  <=>  x$y
    
    x|y     =>   not(x  x $ y
    x < y  =>  not (y < x)          converse false!
    
    $$( (x,y),z ) =  (x,y)$(x,y) and (x,y)$z
                  =  x$x and x$y ...
                  ...
                  = (x,y,z) $ (x,y,z)
                  = $$(x,y,z)

    e and not e  => false
    x|y and x$y  => false
    $$(||(x))  =>  false
    ||($$(x))  =>  false

Example: shared read, exclusive write

Let there be a variable where

    C denotes the constructor
    D denotes the destructor
    M1,...Mm denote functions that modify the variable
    R1,...,Rn denote functions that read the variable

The variable is threadsafe using the following rule:

    !C < (||(R1,...,Rn) $ $$(M1,...Mm)) < !D
    
which means

    C can be called at most once
    C < Ri   for all i
    C < Mi   for all i
    Ri | Rj  for all i,j
    Ri $ Mj  for all i,j
    Mi $ Mj  for all i,j
    Ri < D   for all i
    Mi < D   for all i
    D can be called at most once

Note that we cannot write it like this:

    $$(M1,...Mm,||(R1,...,Rn))
    
This is illogical because it implies

   ||(R1,...,Rn) $ ||(R1,...,Rn)
   
which is self contradictory, because it implies Ri | Rj and also Ri $ Rj.

Sufficient requirements for threadsafe access to a variable

Let the thread safety rules by given by a single expression e.

1.  If e = (e1 < e2),  then recursively check both e1 and e2

2.  if e = $$(m1,...,mn) where each mi are functions then e is safe.

3.  if e = e1 $ e2 then recursively check both e1 and e2

4.  if e = ||(r1,...,rn) then safe as long as each ri only have read access.

5.  e = !x then e is safe

Algebraic rules

    expr1 and expr2     means it is known that the rules implied by expr1 as well as the rules 
                        implied by expr2 must be satisfied.
                        
    expr1 or expr2      means it is known that either the rules implied by expr1 or else the rules 
                        implied by expr2 must be satisfied.
                        
    not expr            means it is known that the rules implied by expr do not need to be 
                        satisfied.

and is commutative and transitive
or is commutative and transitive
not(not p) = p

Y < X   => not(X < Y).  But converse is false!

    X$Y     means       X
    
Example

$$W | $$X | $$(Y,Z) is shorthand for

    W $ W
    X $ X
    Y $ Y
    Y $ Z
    Z $ Z
    W | X
    W | Y
    W | Z
    X | Y
    X | Z