Keywords: transition system, formal reasoning, liveness properties
Units: 24 units
Background
Concurrent systems often have shared resources that can be accessed by no more than one process at any given time. Such resources are called “critical sections”. When multiple processes want to access a critical section, it is the job of “mutual exclusion protocols” to coordinate which process can access first.
To show that a mutual exclusion protocol really works, we need to establish the safety property (any two processes never enter the critical section at the same time), as well as a liveness property (if a process attempts to enter the critical section, then it succeeds eventually).
When proving liveness properties, we always implicitly or explicitly assume some form of “fairness” (e.g. when a process has an always-possible step, then it will eventually take that step). Fairness assumptions guarantee that the whole mutual exclusion protocol would not be brought to a standstill due to a process not progressing its protocol-steps or being shut down unexpectedly. Based on such assumptions, we then go on to reason about the liveness properties of mutual exclusion protocols.
However, there is an argument that the typical fairness assumption is too strong; namely, even when a step is always possible, it is still reasonable for a process not to take that step. Subsequently, a weaker notion called “justness” was proposed [vGH19].
Research Questions and Tasks
To investigate whether the liveness properties of mutual exclusion protocols still hold, when the underlying assumption is weakened from fairness to justness. In particular, this project will look at several common mutual exclusion protocols (such as Peterson’s algorithm), and attempt to prove or disprove their liveness properties using justness assumption.
Requirements: Discrete mathematics related to state-transition systems. Mathematical logic for stating and manipulating properties of programs.