Abstract
We address the problem of fence inference in infinite-state concurrent programs running on relaxed memory models such as TSO and PSO. We present a novel algorithm that can automatically synthesize the necessary fences for infinite-state programs.
Our technique is based on two main ideas: (i) verification with numerical domains: we reduce verification under relaxed models to verification under sequential consistency using integer and boolean variables. This enables us to combine abstraction refinement over booleans with powerful numerical abstractions over the integers. (ii) synthesis with refinement propagation: to synthesize fences for a program P, we combine abstraction refinements used for successful synthesis of programs coarser than P into a new candidate abstraction for P. This “proof reuse” approach dramatically reduces the time required to discover a proof for P.
We implemented our technique and successfully applied it to several challenging concurrent algorithms, including state of the art concurrent work-stealing queues.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Automatic fence insertion in integer programs via predicate abstraction. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 164–180. Springer, Heidelberg (2012)
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer 29, 66–76 (1995)
Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512–532. Springer, Heidelberg (2013)
Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99–115. Springer, Heidelberg (2011)
Burckhardt, S., Alur, R., Martin, M. M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI 2007 (2007)
Chase, D., Lev, Y.: Dynamic circular work-stealing deque. In: SPAA (2005)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978 (1978)
Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 84–104. Springer, Heidelberg (2013)
Frigo, M., Leiserson, C.E., Randall, K.H.: The implementation of the cilk-5 multithreaded language. In: PLDI 1998 (1998)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002 (2002)
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (April 2008)
Huynh, T.Q., Roychoudhury, A.: Memory model sensitive bytecode verification. Form. Methods Syst. Des. 31(3) (December 2007)
Jeannet, B.: The CONCURINTERPROC interprocedural analyzer for concurrent programs, http://pop-art.inrialpes.fr/interproc/concurinterprocweb.cgi
Jeannet, B.: Relational interprocedural verification of concurrent programs. Software and System Modeling 12(2), 285–306 (2013)
Jeannet, B., Miné, A.: apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)
Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings (preliminary version). SIGARCH Comput. Archit. News 36(5), 65–71 (2009)
Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD 2010 (2010)
Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI 2011 (2011)
Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010)
Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 339–353. Springer, Heidelberg (2013)
Liu, F., Nedev, N., Prisadnikov, N., Vechev, M., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI 2012 (2012)
Meshman, Y., Dan, A., Vechev, M., Yahav, E.: Synthesis of memory fences via refinement propagation. Tech. rep.
Michael, M.M., Vechev, M.T., Saraswat, V.A.: Idempotent work stealing. In: PPoPP 2009 (2009)
Norris, B., Demsky, B.: CDSchecker: checking concurrent data structures written with c/c++ atomics. In: OOPSLA 2013 (2013)
Vafeiadis, V., Zappa Nardelli, F.: Verifying fence elimination optimisations. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 146–162. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Meshman, Y., Dan, A., Vechev, M., Yahav, E. (2014). Synthesis of Memory Fences via Refinement Propagation. In: Müller-Olm, M., Seidl, H. (eds) Static Analysis. SAS 2014. Lecture Notes in Computer Science, vol 8723. Springer, Cham. https://doi.org/10.1007/978-3-319-10936-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-10936-7_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10935-0
Online ISBN: 978-3-319-10936-7
eBook Packages: Computer ScienceComputer Science (R0)