JetBrains Research unites scientists working in challenging new disciplines

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: