0
$\begingroup$

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?

| cite | improve this question | |
$\endgroup$
  • $\begingroup$ 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). $\endgroup$ – D.W.♦ Jun 4 '15 at 19:13
  • $\begingroup$ @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. $\endgroup$ – Oper Jun 5 '15 at 9:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.