Jade Alglave
Paul E. McKenney
Abstract
Concurrency in the Linux kernel can be a contentious topic. The Linux kernel mailing list features numerous discussions related to consistency models, including those of the more than 30 CPU architectures supported by the kernel and that of the kernel itself. How are Linux programs supposed to behave? Do they behave correctly on exotic hardware? A formal model can help address such questions. Better yet, an executable model allows programmers to experiment with the model to develop their intuition. Thus we offer a model written in the cat language, making it not only formal, but also executable by the herd simulator. We tested our model against hardware and refined it in consultation with maintainers. Finally, we formalised the fundamental law of the Read-Copy-Update synchronisation mechanism, and proved that one of its implementations satisfies this law.
- Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. 2015. GPU Concurrency: Weak Behaviours and Programming Assumptions ASPLOS 2015. Google Scholar
Digital Library
- Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. Syntax and semantics of the weak consistency model specification language textsfcat. CoRR Vol. abs/1608.07531 (2016). http://arxiv.org/abs/1608.07531Google Scholar
- Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software Computer Aided Verification (CAV) (LNCS), Vol. Vol. 8044. Springer, 141--157.Google Scholar
- Jade Alglave and Luc Maranget. 2011--2017. The textsfdiy7 tool suite. http://diy.inria.fr/. (2011--2017).Google Scholar
- Jade Alglave and Luc Maranget. 2015. Towards a formalisation of the HSA memory model in the textsfcat language. http://www.hsafoundation.com/?ddownload=5381. (2015).Google Scholar
- Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2017 a. A formal model of Linux-kernel memory ordering -- companion webpage. http://diy.inria.fr/linux/. (2017). {Online; accessed 25-December-2017}.Google Scholar
- Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2017 b. A formal kernel memory-ordering model (part 1). (14 April. 2017). https://lwn.net/Articles/718628/Google Scholar
- Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2017 c. A formal kernel memory-ordering model (part 2). (20 April. 2017). https://lwn.net/Articles/720550/Google Scholar
- Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in Weak Memory Models. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15--19, 2010. Proceedings. 258--272. Google ScholarDigital Library
- Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012. Fences in weak memory models (extended version). Formal Methods in System Design Vol. 40, 2 (2012), 170--205. Google ScholarDigital Library
- Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. Vol. 36, 2, Article bibinfoarticleno7 (July. 2014), bibinfonumpages7:1--7:74 pages.bibinfoyear2012. Re: Memory corruption due to word sharing. https://gcc.gnu.org/ml/gcc/2012-02/msg00013.html. (2012). Google ScholarDigital Library
- Linus Torvalds. 2015. Re: {PATCH 4/4} locking: Introduce smp_cond_acquire(). http://lkml.kernel.org/r/CA+55aFyXu5iFJfdm7o-RKUm_9a850iSzeM+whmtUAotkY0EvTw@mail.gmail.com. (2015).Google Scholar
- Linus Torvalds. 2016 a. Re: {RFC}{PATCH} mips: Fix arch_spin_unlock(). https://lkml.org/lkml/2016/2/2/80. (2016).Google Scholar
- Linus Torvalds. 2016 b. Re: {v3,11/41} mips: reuse asm-generic/barrier.h. https://marc.info/?l=linux-kernel&m=145384764324700&w=2. (26 January. 2016).Google Scholar
- Linus Torvalds. 2017 a. Linux Kernel v4.12 (Fearless Coyote). https://www.kernel.org/pub/linux/kernel/v4.x/linux-4.12.tar.xz. (2 July. 2017).Google Scholar
- Linus Torvalds. 2017 b. Re: {GIT PULL rcu/next} RCU commits for 4.13. https://lkml.org/lkml/2017/6/27/1052. (2017).Google Scholar
- Srivatsa Vaddagiri. 2005. {PATCH} Fix RCU race in access of nohz_cpu_mask. http://lkml.iu.edu/hypermail/linux/kernel/0512.0/0976.html. (5 December. 2005).Google Scholar
- Leonid Yegoshin. 2016 a. Re: (v3,11/41) mips: reuse asm-generic/barrier.h. https://marc.info/?l=linux-kernel&m=145263153305591&w=2. (12 January. 2016).Google Scholar
- Leonid Yegoshin. 2016 b. Re: {v3,11/41} mips: reuse asm-generic/barrier.h. https://marc.info/?l=linux-kernel&m=145280444229608&w=2. (14 January. 2016).Google Scholar
- Leonid Yegoshin. 2016 c. Re: {v3,11/41} mips: reuse asm-generic/barrier.h. https://marc.info/?l=linux-kernel&m=145280241129008&w=2. (14 January. 2016).Google Scholar
- Peter Zijlstra. 2013 a. Re: Does Itanium permit speculative stores? https://marc.info/?l=linux-kernel&m=138428080207125. (12 November. 2013).Google Scholar
- Peter Zijlstra. 2013 b. Re: {PATCH v6 4/5} MCS Lock: Barrier corrections. https://marc.info/?l=linux-mm&m=138514629508662&w=2. (2013).Google Scholar
- Peter Zijlstra. 2016. {tip:perf/urgent} perf/core: Fix sys_perf_event_open() vs. hotplug. https://www.spinics.net/lists/kernel/msg2421883.html. (14 January. 2016).Google Scholar
Recommendations
Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel
ASPLOS '18: Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating SystemsConcurrency in the Linux kernel can be a contentious topic. The Linux kernel mailing list features numerous discussions related to consistency models, including those of the more than 30 CPU architectures supported by the kernel and that of the kernel ...
A framework for the assessment of operating systems for small computers
A number of high performance operating systems are now available for small computers on different hardware platforms. These operating systems offer many advanced features formerly reserved for their workstation and minicomputer counterparts. This ...
A detailed performance analysis of UDP/IP, TCP/IP, and M-VIA network protocols using Linux/SimOS
This paper presents a performance study of UDP/IP, TCP/IP, and M-VIA using Linux/SimOS. Linux/SimOS is a Linux operating system port to a complete machine simulator SimOS. A complete machine simulator includes all the system components, such as CPU, ...
Comments