×

zbMATH — the first resource for mathematics

Semantics of concurrent revisions. (English) Zbl 1326.68081
Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 116-135 (2011).
Summary: Enabling applications to execute various tasks in parallel is difficult if those tasks exhibit read and write conflicts. We recently developed a programming model based on concurrent revisions that addresses this challenge in a novel way: each forked task gets a conceptual copy of all the shared state, and state changes are integrated only when tasks are joined, at which time write-write conflicts are deterministically resolved.
In this paper, we study the precise semantics of this model, in particular its guarantees for determinacy and consistency. First, we introduce a revision calculus that concisely captures the programming model. Despite allowing concurrent execution and locally nondeterministic scheduling, we prove that the calculus is confluent and guarantees determinacy. We show that the consistency guarantees of our calculus are a logical extension of snapshot isolation with support for conflict resolution and nesting. Moreover, we discuss how custom merge functions can provide stronger guarantees for particular data types that are tailored to the needs of the application.
Finally, we show we can visualize the nonlinear history of state in our computations using revision diagrams that clarify the synchronization between tasks and allow local reasoning about state updates.
For the entire collection see [Zbl 1213.68027].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q55 Semantics in the theory of computing
68Q65 Abstract data types; algebraic specification
Software:
Grace
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aditya, S., Arvind, Augustsson, L., Maessen, J.-W., Nikhil, R.: Semantics of pH: A Parallel Dialect of Haskell. In: Hudak, P. (ed.) Proc. Haskell Workshop, La Jolla, CA, USA, pp. 35–49 (June 1995)
[2] Allen, E., Chase, D., Flood, C., Luchangco, V., Maessen, J.-W., Ryu, S., Steele Jr., G.: Project fortress: A multicore language for multicore processors. In: Linux Mag. (September 2007)
[3] Baldassin, A., Burckhardt, S.: Lightweight software transactions for games. In: Workshop on Hot Topics in Parallelism, HotPar (2009)
[4] Berenson, H., Bernstein, P., Gray, J., Melton, J., O’Neil, E., O’Neil, P.: A critique of ANSI SQL isolation levels. In: Proceedings of SIGMOD, pp. 1–10 (1995) · doi:10.1145/223784.223785
[5] Berger, E., Yang, T., Liu, T., Novark, G.: Grace: Safe multithreaded programming for C/C++. In: OOPSLA (2009)
[6] Blelloch, G., Chatterjee, S., Hardwick, J., Sipelstein, J., Zagha, M.: Impl. of a portable nested data-parallel language. Journal of Par. and Dist. Comp. 21(1), 4–14 (1994) · doi:10.1006/jpdc.1994.1038
[7] Bocchino, R., Adve, V., Dig, D., Adve, S., et al.: A type and effect system for deterministic parallel java. In: OOPSLA (2009) · doi:10.1145/1640089.1640097
[8] Burckhardt, S., Baldassin, A., Leijen, D.: Concurrent programming with revisions and isolation types. In: OOPSLA (October 2010) · doi:10.1145/1869459.1869515
[9] Burckhardt, S., Leijen, D.: Semantics of concurrent revisions. Technical Report MSR-TR-2010-94, Microsoft Research (2010) · Zbl 1326.68081
[10] Denning, P., Dennis, J.: The resurgence of parallelism. Commun. ACM 53(6) (2010) · Zbl 05748235 · doi:10.1145/1743546.1743560
[11] Fekete, A., Liarokapis, D., O’Neil, E., O’Neil, P., Shasha, D.: Making snapshot isolation serializable. ACM Trans. Database Syst. 30(2), 492–528 (2005) · Zbl 05457020 · doi:10.1145/1071610.1071615
[12] Flanagan, C., Felleisen, M.: The semantics of future and its use in program optimization, Rice University, pp. 209–220 (1995) · doi:10.1145/199448.199484
[13] Frigo, M., Halpern, P., Leiserson, C.E., Lewin-Berlin, S.: Reducers and other cilk++ hyperobjects. In: Sym. on Par. Algorithms and Architectures, SPAA, pp. 79–90 (2009) · doi:10.1145/1583991.1584017
[14] Frigo, M., Leiserson, C., Randall, K.: The implementation of the Cilk-5 multithreaded language. In: Programming Language Design and Impl., PLDI, pp. 212–223 (1998) · doi:10.1145/277650.277725
[15] Harris, T., Cristal, A., Unsal, O., Ayguadé, E., Gagliardi, F., Smith, B., Valero, M.: Transactional memory: An overview. IEEE Micro 27(3), 8–29 (2007) · Zbl 05334601 · doi:10.1109/MM.2007.63
[16] Herlihy, M., Koskinen, E.: Transactional boosting: a methodology for highly-concurrent transactional objects. In: Principles and Practice of Parallel Programming, PPoPP, pp. 207–216 (2008) · doi:10.1145/1345206.1345237
[17] Herlihy, M., Wing, J.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990) · doi:10.1145/78969.78972
[18] Huet, G.: Confluent reductions: Abstract properties and applications in term rewriting systems. J. ACM 27(4) (October 1980) · Zbl 0458.68007 · doi:10.1145/322217.322230
[19] Koskinen, E., Parkinson, M., Herlihy, M.: Coarse-grained transactions. In: Principles of Programming Languages, POPL, pp. 19–30 (2010) · Zbl 1312.68143 · doi:10.1145/1706299.1706304
[20] Kulkarni, M., Pingali, K., Walter, B., Ramanarayanan, G., Bala, K., Chew, L.: Optimistic parallelism requires abstractions. In: PLDI (2007) · doi:10.1145/1250734.1250759
[21] Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp. C-28(9), 690–691 (1979) · Zbl 0419.68045 · doi:10.1109/TC.1979.1675439
[22] Larus, J., Rajwar, R.: Transactional Memory. Morgan & Claypool (2007)
[23] Lee, J., Palsberg, J.: Featherweight x10: a core calculus for async-finish parallelism. In: Principles and Practice of Parallel Programming, PPoPP 2010 (2010) · doi:10.1145/1693453.1693459
[24] Martin, A., Birrell, A., Harris, T., Isard, M.: Semantics of transactional memory and automatic mutual exclusion. In: Principles of Prog. Lang. POPL, pp. 63–74 (2008) · Zbl 1295.68149
[25] Moreau, L.: The semantics of scheme with future. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, pp. 146–156 (1996) · Zbl 1345.68066 · doi:10.1145/232627.232644
[26] Bernstein, P.A., Goodman, N.: Multiversion concurrency control–theory and algorithms. ACM Trans. Database Syst. 8(4), 465–483 (1983) · Zbl 0531.68060 · doi:10.1145/319996.319998
[27] Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley, Reading (1987)
[28] Pratikakis, P., Spacco, J., Hicks, M.: Transparent proxies for java futures. SIGPLAN Not. 39(10), 206–223 (2004) · doi:10.1145/1035292.1028994
[29] Randall, K.: Cilk: Efficient Multithreaded Computing. PhD thesis, Dept. of Electrical Engineering and Computer Science. MIT, Cambridge (1998)
[30] Riegel, T., Fetzer, C., Felber, P.: Snapshot isolation for software transactional memory. In: Workshop on Transactional Computing, TRANSACT (2006) · Zbl 1188.68101
[31] Steele, G.: Parallel programming and parallel abstractions in fortress. In: Hagiya, M. (ed.) FLOPS 2006. LNCS, vol. 3945, pp. 1–1. Springer, Heidelberg (2006) · Zbl 05148608 · doi:10.1007/11737414_1
[32] Welc, A., Jagannathan, S., Hosking, A.: Safe futures for java. In: OOPSLA, pp. 439–453 (2005) · doi:10.1145/1094811.1094845
[33] Welc, A., Saha, B., Adl-Tabatabai, A.-R.: Irrevocable transactions and their applications. In: Symposium on Parallel Algorithms and Architectures, SPAA, pp. 285–296 (2008)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.