Abstract
Atomicity is an important generic specification that assures that a programmer can pretend blocks occur sequentially in any execution. We define a notion of atomicity based on causality. We model the control flow of a program with threads using a Petri net that naturally abstracts data, and faithfully captures the independence and interaction between threads. The causality between events in the partially ordered executions of the Petri net is used to define the notion of causal atomicity. We show that causal atomicity is a robust notion that many correct programs adopt, and show how we can effectively check causal atomicity using Petri net tools based on unfoldings, which exploit the concurrency in the net to yield automatic partial-order reduction in the state-space.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1-2), 167–188 (2000)
Bernstein, P., Hadzilacos, V., Goodman, N.: Concurrency control and recovery in database systems. Addison-Wesley Longman (1987)
Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 334–349. Springer, Heidelberg (2006)
Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific Publishing Co., Singapore (1995)
Esparza, J., Romer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 87–106. Springer, Heidelberg (1996)
Eswaran, K., Gray, J., Lorie, R., Traiger, I.: The notions of consistency and predicate locks in a database system. Commun. ACM 19(11), 624–633 (1976)
Flanagan, C.: Verifying commit-atomicity using model-checking. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 252–266. Springer, Heidelberg (2004)
Flanagan, C., Freund, S.: Atomizer: a dynamic atomicity checker for multithreaded programs. In: POPL, pp. 256–267 (2004)
Flanagan, C., Freund, S., Qadeer, S.: Exploiting purity for atomicity. IEEE Trans. Software Eng. 31(4), 275–291 (2005)
Flanagan, C., Qadeer, S.: Types for atomicity. In: TLDI, pp. 1–12 (2003)
Flé, M., Roucairol, G.: On serializability of iterated transactions. In: PODC, pp. 194–200 (1982)
Grahlmann, B.: The PEP tool. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 440–443. Springer, Heidelberg (1997)
Hatcliff, J., Robby, Dwyer, M.: Verifying atomicity specifications for concurrent object-oriented software using model-checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 175–190. Springer, Heidelberg (2004)
Jensen, K.: Coloured Petri nets: basic concepts, analysis methods and practical use, 2nd edn., vol. 1. Springer, London (1996)
Lipton, R.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Lodaya, K., Mukund, M., Ramanujam, R., Thiagarajan, P.S.: Models and logics for true concurrency. Technical Report TCS–90–3, School of Mathematics Internal (1990)
McMillan, K.: A technique of state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (1995)
Nielsen, M., Plotkin, G., Winsker, G.: Peri nets, event structures and domains — part i. Theoretical Computer Science 13, 85–108 (1981)
Papadimitriou, C.: The theory of database concurrency control. Computer Science Press, Inc., New York (1986)
Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI, pp. 14–24 (2004)
Silberschatz, A., Korth, H., Sudarshan, S.: Database Systems Concepts, 5th edn. McGraw-Hill, New York (2005)
Wang, L., Stoller, S.: Run-time analysis for atomicity. Electr. Notes Theor. Comput. Sci. 89(2) (2003)
Wang, L., Stoller, S.: Static analysis of atomicity for programs with non-blocking synchronization. In: PPOPP, pp. 61–71 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Farzan, A., Madhusudan, P. (2006). Causal Atomicity. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_30
Download citation
DOI: https://doi.org/10.1007/11817963_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)