Suppose I have programs A and B defined in this way:
A = let F:Tf = (fn f:T ==> (fn(x:unit => x || fx))) in (fix.F)(m=!l+1;l=!m+1)
B = let F:Tf = (fn f:T ==> (fn(x:unit => x;fx))) in (fix.F)(m=!l+1;l=!m+1)
where ||
indicates concurrency and ;
is the sequence symbol.
How can I prove (not formally) whether these two programs are simulated or bisimulated?
How can I prove formally if these programs are going to data race?