Overview of rely/Guarantee Jones 83 r: acceptable environment transitions g: state transitions made by the thread Thread1 Thread2 X=31 Y=Y 2: Nobody else would update y Noboru else tyyurrpuatex X= 81:0 2:0 I guarantee I would not touch x I guaractnpartiatHtytmterference Constraints) g2 cr1 and g1 cr2[Jones'83] Overview of Rely/Guarantee • r: acceptable environment transitions • g: state transitions made by the thread Thread1 Thread2 Nobody else would update x I guarantee I would not touch y Nobody else would update y I guarantee I would not touch x Compatibility (Interference Constraints): g2  r1 and g1  r2 r1:  x = x’ ’ r2:  y = y’ ’ g1:  y = y’ ’ g2:  x = x’ ’