IMSc Webinar

Consistency framework for relaxed memory models.

Prakash Saivasan

IMSc

Webinar; Join at https://bluejeans.com/789726971. Programmers usually assume that all memory access to shared memory are done sequentially. Such memory accesses are guaranteed only by the strict memory models such as sequential consistency [Lamport’79]. For performance reasons most modern day processors relax the ordering of the memory access. For example, the relaxation may allow a write to be delayed past a subsequent read. In this talk we will survey some well-known relaxed memory models and some results there in. We will then see how to obtain provable optimal algorithms to check consistency for various memory models, under the assumption of data-independence. Given executions of concurrent programs over a shared memory system, the consistency problem asks whether there is an execution that is consistent with the intended behaviour of the memory model. The data-independence assumes that no two write occur with the same value. Towards an upper bound, we first obtain a O*(2^k) consistency algorithm for a generalised frame work, assuming data-independence. Here $k$ is the number of values that occur in the given executions. We obtain the consistency algorithms for SC, PSO and TSO by instantiating them on the generalised framework. Relying on ETH, we prove the optimality of these algorithms.