Concurrent programming is known to be quite hard. It is made even harder by the fact that, very often, the execution models of the machines we run our software on are not precisely defined.
This lecture is a tutorial on the herd tool and the cat language, in which one can define consistency models, i.e. execution models of concurrent and distributed systems.
By the end of this lecture, you should be able to build several models:
- Sequential Consistency
- Total Store Order
- a model similar in spirit to ARM
- a model similar in spirit to Nvidia GPUs
- a model inspired by C++.
Most of the lecture is going to be interactive, using the herd tool. For this tutorial to go smoothly, I would suggest to download the herd tool and install it beforehand.
- J. Alglave. Herding cats. Slides from the course at EWSCS '19.
- The herdtools toolset, including diy, litmus, herd: diy.inria.fr, github.com/herd/herdtools7/
- Litmus tests for this course [.litmus files]
- Videos from the lectures (large, unedited files) [mp4, password-protected]
- J. Alglave. Modeling of architectures. In M. Bernardo, E. B. Johnsen, eds., Advanced Lectures from SFM 2015, v. 9104 of Lect. Notes in Comput. Sci., pp. 97-145. Springer, 2015. [doi, pdf]
- J. Alglave, L. Maranget, M. Tautschnig. Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., v. 36, n. 2, article 7, 2014. [doi, pdf]
- J. Alglave, L. Maranget, P. E. McKenney, A. Parri, A. S. Stern. Frightening small children and disconcerting grown-ups: concurrency in the Linux kernel. In Proc. of ASPLOS 2018, pp. 405-418. ACM, 2018. [doi, pdf]
April 10, 2020 22:39 Europe/Helsinki (GMT +03:00)
local organizers, ewscs19(at)cs.ioc.ee
EWSCS'19 page: http://cs.ioc.ee/ewscs/2019/