Liveness under weak memory
Liveness proofs of concurrent programs often rely on thread fairness which is an assumption that every active thread will be eventually scheduled. Yet for execution under weak memory, such requirement turns out to be insufficient; in particular, to prove termination one should also require so-called memory fairness. In this talk, we'll consider how the introduction of such a requirement changes the definitions of common memory models. Also, we will show that for declarative models memory fairness can be defined in a uniform fashion and will use that definition to prove spinlock termination.
Speaker: Egor Namakonov
The seminar will be held in google meet on Monday, November 30, at 17:30 (google meet room: https://meet.google.com/myu-dhmz-gvu)