Abstract
Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency. As the fences’ semantics may be subtle, the automation of their placement is highly desirable. But precise methods for restoring consistency do not scale to deployed systems code. We choose to trade some precision for genuine scalability: our technique is suitable for large code bases. We implement it in our new musketeer tool, and detail experiments on more than 350 executables of packages found in Debian Linux 7.1, e.g. memcached (about 10000 LoC).
Supported by SRC/2269.002, EPSRC/H017585/1 and ERC/280053.
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
Power ISA Version 2.06 (2009)
Information technology – Programming languages – C. In: BS ISO/IEC 9899:2011 (2011)
Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: memorax, a precise and sound tool for automatic fence insertion under TSO. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 530–536. Springer, Heidelberg (2013)
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer 29(12), 66–76 (1995)
Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50–66. Springer, Heidelberg (2011)
Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 258–272. Springer, Heidelberg (2010)
Alglave, J., Kroening, D., Lugton, J., Nimal, V., Tautschnig, M.: Soundness of data flow analyses for weak memory models. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 272–288. Springer, Heidelberg (2011)
Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don’t sit on the fence: A static analysis approach to automatic fence insertion. CoRR abs/1312.1411 (2013)
Bouajjani, A., Meyer, R., Möhlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 428–440. Springer, Heidelberg (2011)
Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013)
Chase, D., Lev, Y.: Dynamic circular work-stealing deque. In: SPAA, pp. 21–28. ACM (2005)
Detlefs, D.L., Flood, C.H., Garthwaite, A.T., Martin, P.A., Shavit, N.N., Steele Jr., G.L.: Even better DCAS-based concurrent deques. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 59–73. Springer, Heidelberg (2000)
Dice, D.: (November 2009), https://blogs.oracle.com/dave/entry/a_race_in_locksupport_park
Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)
Fang, X., Lee, J., Midkiff, S.P.: Automatic fence insertion for shared memory multiprocessing. In: International Conference on Supercomputing (ICS), pp. 285–294. ACM (2003)
Frigo, M., Leiserson, C.E., Randall, K.H.: The implementation of the Cilk-5 multithreaded language. In: PLDI, pp. 212–223. ACM (1998)
Krishnamurthy, A., Yelick, K.A.: Analyses and optimizations for shared address space programs. J. Par. Dist. Comp. 38(2) (1996)
Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 111–119. IEEE (2010)
Kuperstein, M., Vechev, M.T., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI, pp. 187–198 (2011)
Lamport, L.: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Comput. 46(7) (1979)
Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1) (1987)
Lee, J., Padua, D.A.: Hiding relaxed memory consistency with a compiler. IEEE Transactions on Computers 50, 824–833 (2001)
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.T., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI, pp. 429–440. ACM (2012)
Marino, D., Singh, A., Millstein, T.D., Musuvathi, M., Narayanasamy, S.: A case for an SC-preserving compiler. In: PLDI, pp. 199–210. ACM (2011)
Michael, M.M., Vechev, M.T., Saraswat, V.A.: Idempotent work stealing. In: Principles and Practice of Parallel Programming (PPOPP), pp. 45–54. ACM (2009)
Norris, B., Demsky, B.: CDSchecker: checking concurrent data structures written with C/C++ atomics. In: Object Oriented Programming Systems Languages & Applications (OOPSLA), pp. 131–150 (2013)
Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009)
Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)
Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. TOPLAS 10 ( 2 ), 282–312 (1988)
Sparc Architecture Manual Version 9 (1994)
Sura, Z., Fang, X., Wong, C.-L., Midkiff, S.P., Lee, J., Padua, D.A.: Compiler techniques for high performance sequentially consistent Java programs. In: PPOPP, pp. 2–13. ACM (2005)
Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: ICS, pp. 621–626 (1988)
Tarjan, R.: Enumeration of the elementary circuits of a directed graph. SIAM J. Comput. 2(3), 211–216 (1973)
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
Alglave, J., Kroening, D., Nimal, V., Poetzl, D. (2014). Don’t Sit on the Fence. In: Biere, A., Bloem, R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham. https://doi.org/10.1007/978-3-319-08867-9_33
Download citation
DOI: https://doi.org/10.1007/978-3-319-08867-9_33
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08866-2
Online ISBN: 978-3-319-08867-9
eBook Packages: Computer ScienceComputer Science (R0)