Ordering of events in two-process concurrent system
Jayasri Banerjee, Anup Bandyopadhyay, Ajit Kumar Mandal · ACM SIGSOFT Software Engineering Notes · 2007
Dijkstra's weakest precondition calculus is extended to capture temporal ordering in concurrent systems. This is done by defining temporal ordering predicates that is used to describe necessary conditions. A new logical connective, viz., "implies in the past" is also defined to describe the cause and effect relationships. Ordering mechanism used in Peterson's two process mutual exclusion algorithm is explained by proving a theorem.