Advertisement

Predicate Abstraction for Relaxed Memory Models

  • Andrei Marian Dan
  • Yuri Meshman
  • Martin Vechev
  • Eran Yahav
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

Abstract

We present a novel approach for predicate abstraction of programs running on relaxed memory models. Our approach consists of two steps.

First, we reduce the problem of verifying a program P running on a memory model M to the problem of verifying a program P M that captures an abstraction of M as part of the program.

Second, we present a new technique for discovering predicates that enable verification of P M . The core idea is to extrapolate from the predicates used to verify P under sequential consistency. A key new concept is that of cube extrapolation: it successfully avoids exponential state explosion when abstracting P M .

We implemented our approach for the x86 TSO and PSO memory models and showed that predicates discovered via extrapolation are powerful enough to verify several challenging concurrent programs. This is the first time some of these programs have been verified for a model as relaxed as PSO.

Keywords

Model Check Shared Variable Global Variable Memory Model Sequential Consistency 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Andrews, G.R.: Concurrent programming - principles and practice. Benjamin/Cummings (1991)Google Scholar
  4. 4.
    Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL (2010)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI (2001)Google Scholar
  7. 7.
    Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI (2007)Google Scholar
  8. 8.
    Burckhardt, S., Baldassin, A., Leijen, D.: Concurrent programming with revisions and isolation types. In: OOPSLA (2010)Google Scholar
  9. 9.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)Google Scholar
  10. 10.
    Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. Tech. repGoogle Scholar
  11. 11.
    Das, S., Dill, D.L., Park, S.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  12. 12.
    Dijkstra, E.: Cooperating sequential processes, TR EWD-123. Tech. rep., Technological University, Eindhoven (1965)Google Scholar
  13. 13.
    Donaldson, A., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 356–371. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  14. 14.
    Dubois, M., Scheurich, C., Briggs, F.A.: Memory access buffering in multiprocessors. In: ISCA (1986)Google Scholar
  15. 15.
    Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL (2002)Google Scholar
  16. 16.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  17. 17.
    Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  18. 18.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)Google Scholar
  19. 19.
    Huynh, T.Q., Roychoudhury, A.: Memory model sensitive bytecode verification. Form. Methods Syst. Des. (2007)Google Scholar
  20. 20.
    IBM. Power ISA v.2.05. (2007)Google Scholar
  21. 21.
    Jonsson, B.: State-space exploration for concurrent algorithms under weak memory orderings. SIGARCH Comput. Archit. News (2008)Google Scholar
  22. 22.
    Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2010)Google Scholar
  23. 23.
    Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI (2011)Google Scholar
  24. 24.
    Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM (1974)Google Scholar
  25. 25.
    Park, S., Dill, D.L.: An executable specification and verifier for relaxed memory order. IEEE Trans. on Computers 48 (1999)Google Scholar
  26. 26.
    Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3) (1981)Google Scholar
  27. 27.
    Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-cc multiprocessor machine code. In: POPL (2009)Google Scholar
  28. 28.
    SPARC International, Inc. The SPARC architecture manual (version 9). Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1994)Google Scholar
  29. 29.
    Szymanski, B.K.: A simple solution to Lamport’s concurrent programming problem with linear wait. In: ICS (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Andrei Marian Dan
    • 1
  • Yuri Meshman
    • 2
  • Martin Vechev
    • 1
  • Eran Yahav
    • 2
  1. 1.ETH ZurichSwitzerland
  2. 2.TechnionIsrael

Personalised recommendations