Equivalence Are The two Systems Equivalent? collect They are equivalent as C automata collect-coftee As concurrent systems they are not equivalent because the ways buyers interact with them are collect-tea different A collect-coffe Observational equivalence coffee 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 37 Equivalence ◼ Are The Two Systems Equivalent? ◼ They are equivalent as automata ◼ As concurrent systems they are not equivalent, because the ways buyers interact with them are different ◼ Observational Equivalence 1c 1c tea coffee collect-tea collect-coffee collect-tea collect-coffee tea coffee 1c
Example III: Concurrent Program Sequential Programs Concurrent Programs X:=2 X:=2|X:=2 X:=1;X=Ⅹ+1 (X:=1;X=X+1)X:=2 Both Programs Assigns The results are 2toⅩ Nondeterministic a TwO Programs are TWo Programs are not Equivalent Equivalent a Interleaving semantics 2021年1月27日星期三上海交通大学计算机系 BASICS实验室 38
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 38 Example III: Concurrent Program ◼ Sequential Programs ◼ X:=2 ◼ X:=1; X:=X+1 ◼ Both Programs Assigns 2 to X ◼ Two Programs are Equivalent ◼ Concurrent Programs ◼ X:=2 | X:=2 ◼ (X:=1; X:=X+1) | X:=2 ◼ The Results are Nondeterministic ◼ Two Programs are not Equivalent ◼ Interleaving semantics
Example IV: A Unit Transmitter The transmitter receives a message through in It sends out a message through out Repeat n ou C C些in(x).C'(x) C()= out(a).C in (a)out(e).C 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 39 Example IV: A Unit Transmitter ◼ The transmitter receives a message through in ◼ It sends out a message through out ◼ Repeat C in out
Connecting Unit Transmitter n-times In out C C How does it behave? 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 40 Connecting Unit Transmitter C in out C C ..... How does it behave? n-times
Example v: transmitter with Acknowledgment The transmitter receives a message through in It sends out a message through out It receives acknowledgment through ackout It sends acknowledgment through ackin Repeat In ou ackin ackout 2021年1月27日星期三上海交通大学计算机系 BASICS实验室
2021年1月27日星期三 上海交通大学计算机系BASICS实验室 41 Example V: Transmitter with Acknowledgment ◼ The transmitter receives a message through in ◼ It sends out a message through out ◼ It receives acknowledgment through ackout ◼ It sends acknowledgment through ackin ◼ Repeat D in out ackin ackout