critical_bad.csp

var Thread0inside  = 0;
var Thread1inside  = 0;

ThreadZero() = 
    [!(Thread1inside == 1)]
    T0Start
    ->CriticalSectionZero{Thread0inside = 1}
    ->T0End{Thread0inside = 0}
    ->OtherStuffZero
    ->ThreadZero();

ThreadOne() = 
  [!(Thread0inside == 1)]
   T1Start
    ->CriticalSectionOne{Thread1inside = 1}
    ->T1End{Thread1inside = 0}
    ->OtherStuffOne
    ->ThreadOne();

System = ThreadZero() || ThreadOne();

#assert System deadlockfree;
#define badstatus (Thread0inside==1 && Thread1inside == 1);
#assert System reaches badstatus;

critical_bad.go

package main
import "fmt"
import "time"

var Thread0inside int = 0;
var Thread1inside int = 0;

func ThreadZero() {
  for i:=0; i<10; i++{
    for Thread1inside == 1 {}
    //time.Sleep(time.Nanosecond)
    Thread0inside = 1;
    CriticalSectionZero()
    Thread0inside = 0;
    OtherStuffZero();
  }
}

func ThreadOne() {
  for i:=0; i<10; i++{
    for Thread0inside == 1 {}
    //time.Sleep(time.Nanosecond)
    Thread1inside = 1;
    CriticalSectionOne()
    Thread1inside = 0;
    OtherStuffOne();
  }
}

func CriticalSectionZero() {
    for r:=0; r<5;r++ {
       fmt.Printf("CriticalSectionZero(%d)\n", r)
       time.Sleep(100*time.Millisecond)
    }
}
func CriticalSectionOne() {
    for r:=0; r<5;r++ {
       fmt.Printf("                                   CriticalSectionOne(%d)\n", r)
       time.Sleep(100*time.Millisecond)
    }
}
func OtherStuffZero() {
    fmt.Printf("OtherStuffZero\n")
}
func OtherStuffOne() {
    fmt.Printf("                                      OtherStuffOne\n")
}

func main() {
   go ThreadOne()
   go ThreadZero()
   time.Sleep(10000*time.Millisecond)
}