# How to check if two program are simulated or bisimulated?

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?

• What have you tried? Where did you get stuck? What research have you done? What specifically are you stuck on? What sources have you read? We want to help you understand concepts, but doing your exercise for you won't help you (or anyone). – D.W. Jun 4 '15 at 19:13
• @D.W. i don't want you to do my excersise. i just want you to help me to understand this problem. I've tried to apply operational semantics rules in CBN to find a result but i get stucked in fix rule and i don't even know if that's the right procedure to solve the first problem. For the second problem i've no idea on how to prove formally if this programs contains data race. I think i need some examples but i can't find anything online. I've read Semantics of Programming Languages - Sam Stanton. – Oper Jun 5 '15 at 9:28