A formal semantics of nested atomic sections with thread escape. (English) Zbl 1387.68048
Summary: The multi-core trend is widening the gap between programming languages and hardware. Taking parallelism into account in the programs is necessary to improve performance. Unfortunately, current mainstream programming languages fail to provide suitable abstractions to do so. The most common pattern relies on the use of mutexes to ensure mutual exclusion between concurrent accesses to a shared memory. However, this model is error-prone and scales poorly by lack of modularity. Recent research proposes atomic sections as an alternative. The user simply delimits portions of code that should be free from interference. The responsibility for ensuring interference freedom is left either to the compiler or to the run-time system. In order to provide enough modularity, it is necessary that both atomic sections could be nested and threads could be forked inside an atomic section. In this paper, we focus on the semantics of programming languages providing these features. More precisely, without being tied to a specific programming language, we consider program traces satisfying some basic well-formedness conditions. Our main contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is described.
Keywords:
atomic sections; well-synchronisation; atomicity; program traces; formal semantics; proof assistantReferences:
| [3] | Larus, J.; Kozyrakis, C., Transactional memory, Commun ACM, 51, 7, 80-88 (2008) |
| [4] | Cascaval, C.; Blundell, C.; Michael, M.; Cain, H. W.; Wu, P.; Chiras, S., Software transactional memoryWhy is it only a research toy?, Commun ACM, 51, 11, 40-46 (2008) |
| [5] | Dragojević, A.; Felber, P.; Gramoli, V.; Guerraoui, R., Why STM can be more than a research toy?, Commun ACM, 54, 70-77 (2011) |
| [9] | Drepper, U., Parallel programming with transactional memory, Commun ACM, 52, 38-43 (2009) |
| [11] | Moss, J. E.B.; Hosking, A. L., Nested transactional memorymodel and architecture sketches, Sci Comput Program, 63, 186-201 (2006) · Zbl 1119.68043 |
| [15] | Bertot, Y.; Castéran, P., Interactive theorem proving and program development (2004), Springer · Zbl 1069.68095 |
| [17] | Herlihy, M.; Moss, J. E.B., Transactional memoryarchitectural support for lock-free data structures, SIGARCH Comput Archit News, 21, 2, 289-300 (1993) |
| [22] | Bieniusa, A.; Thiemann, P., Proving isolation properties for software transactional memory, (Barthe, G., ESOP. Lecture Notes in Computer Science, vol. 6602 (2011), Springer: Springer Saarbrücken, Germany), 38-56 · Zbl 1326.68078 |
| [24] | Jagannathan, S.; Vitek, J.; Welc, A.; Hosking, A., A transactional object calculus, Sci Comput Program, 57, 164-186 (2005) · Zbl 1076.68021 |
| [26] | Martin, M.; Blundell, C.; Lewis, E., Subtleties of transactional memory atomicity semantics, IEEE Comput Archit Lett, 5, 2, 17 (2006) |
| [27] | Papadimitriou, C. H., The serializability of concurrent database updates, J ACM, 26, 4, 631-653 (1979) · Zbl 0419.68036 |
| [29] | Gonthier, G., Formal proof—the four-color theorem, Not Am Math Soc, 55, 11, 1382-1393 (2008) · Zbl 1195.05026 |
| [32] | Chlipala, A., Certified programming with dependent types (2014), MIT Press |
| [35] | Afek, Y.; Korland, G.; Zilberstein, A., Lowering STM overhead with static analysis, (Cooper, K.; Mellor-Crummey, J.; Sarkar, V., Languages and Compilers for Parallel Computing, Lecture Notes in Computer Science, vol. 6548 (2011), Springer: Springer Fort Collins, CO, USA), 31-45 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
