Document Open Access Logo

Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages

Authors Frank S. de Boer, Einar Broch Johnsen , Rudolf Schlatte, Silvia Lizeth Tapia Tarifa , Lars Tveito

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.10.pdf
  • Filesize: 0.56 MB
  • 18 pages

Document Identifiers

Author Details

Frank S. de Boer
  • CWI Amsterdam, The Netherlands
Einar Broch Johnsen
  • Department of Informatics, University of Oslo, Norway
Rudolf Schlatte
  • Department of Informatics, University of Oslo, Norway
Silvia Lizeth Tapia Tarifa
  • Department of Informatics, University of Oslo, Norway
Lars Tveito
  • Department of Informatics, University of Oslo, Norway

Cite AsGet BibTex

Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito. Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.Gabbrielli.10

Abstract

This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automated static analysis
  • Software and its engineering → Software testing and debugging
  • Software and its engineering → Semantics
  • Theory of computation → Semantics and reasoning
Keywords
  • Testing
  • Symbolic Traces
  • Guarded Commands
  • Partial Order Reduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Source sets: A foundation for optimal dynamic partial order reduction. J. ACM, 64(4):25:1-25:49, 2017. URL: https://doi.org/10.1145/3073408.
  2. Gul Agha. Actors: a model of concurrent computation in distributed systems. MIT Press, 1986. Google Scholar
  3. Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gómez-Zamalloa, and Peter J. Stuckey. Context-sensitive dynamic partial order reduction. In Rupak Majumdar and Viktor Kuncak, editors, Proc. 29th International Conference on Computer Aided Verification (CAV 2017), Part I, volume 10426 of Lecture Notes in Computer Science, pages 526-543. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_26.
  4. Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Systematic testing of actor systems. Softw. Test. Verification Reliab., 28(3), 2018. URL: https://doi.org/10.1002/stvr.1661.
  5. Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. SYCO: a systematic testing tool for concurrent objects. In Ayal Zaks and Manuel V. Hermenegildo, editors, Proc. 25th International Conference on Compiler Construction (CC 2016), pages 269-270. ACM, 2016. URL: https://doi.org/10.1145/2892208.2892236.
  6. Gregory R. Andrews. Concurrent programming - principles and practice. Benjamin/Cummings, 1991. Google Scholar
  7. Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog. Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, 3 edition, 2009. URL: https://doi.org/10.1007/978-1-84882-745-5.
  8. Thomas Ball, Vladimir Levin, and Sriram K. Rajamani. A decade of software model checking with SLAM. Commun. ACM, 54(7):68-76, 2011. URL: https://doi.org/10.1145/1965724.1965743.
  9. Nikolaos Bezirgiannis, Frank S. de Boer, Einar Broch Johnsen, Ka I Pun, and Silvia Lizeth Tapia Tarifa. Implementing SOS with active objects: A case study of a multicore memory system. In Proc. 22nd Intl. Conf. on Fundamental Approaches to Software Engineering (FASE 2019), volume 11424 of Lecture Notes in Computer Science, pages 332-350. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-16722-6_20.
  10. Frank De Boer, Vlad Serbanescu, Reiner Hähnle, Ludovic Henrio, Justine Rochas, Crystal Chang Din, Einar Broch Johnsen, Marjan Sirjani, Ehsan Khamespanah, Kiko Fernandez-Reyes, and Albert Mingkun Yang. A survey of active object languages. ACM Comput. Surv., 50(5):76:1-76:39, October 2017. URL: https://doi.org/10.1145/3122848.
  11. Stephan Brandauer, Elias Castegren, Dave Clarke, Kiko Fernandez-Reyes, Einar Broch Johnsen, Ka I. Pun, S. Lizeth Tapia Tarifa, Tobias Wrigstad, and Albert Mingkun Yang. Parallel objects for multicores: A glimpse at the parallel language Encore. In Marco Bernardo and Einar Broch Johnsen, editors, Formal Methods for Multicore Programming, volume 9104 of Lecture Notes in Computer Science, pages 1-56. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-18941-3_1.
  12. Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavattaro. Replication vs. recursive definitions in channel based calculi. In Proc. 30th International Colloquium on Automata, Languages and Programming (ICALP 2003), volume 2719 of Lecture Notes in Computer Science, pages 133-144. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-27836-8_28.
  13. Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavattaro. Comparing recursion, replication, and iteration in process calculi. In Proc. 31st International Colloquium on Automata, Languages and Programming (ICALP 2004), volume 3142 of Lecture Notes in Computer Science, pages 307-319. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_28.
  14. Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavattaro. On the expressive power of recursion, replication and iteration in process calculi. Math. Struct. Comput. Sci., 19(6):1191-1222, 2009. URL: https://doi.org/10.1017/S096012950999017X.
  15. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. EXE: automatically generating inputs of death. In Ari Juels, Rebecca N. Wright, and Sabrina De Capitani di Vimercati, editors, Proc. 13th ACM Conf. on Computer and Communications Security (CCS'06), pages 322-335. ACM, 2006. URL: https://doi.org/10.1145/1180405.1180445.
  16. Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. Commun. ACM, 56(2):82-90, 2013. URL: https://doi.org/10.1145/2408776.2408795.
  17. Denis Caromel, Ludovic Henrio, and Bernard Serpette. Asynchronous and deterministic objects. In Proc. 31st Symposium on Principles of Programming Languages (POPL 2004), pages 123-134. ACM Press, 2004. URL: https://doi.org/10.1145/964001.964012.
  18. Maria Christakis. Narrowing the Gap between Verification and Systematic Testing. PhD thesis, ETH Zurich, 2015. Google Scholar
  19. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. MIT Press, 2001. URL: https://doi.org/10.3233/978-1-60750-711-6-260.
  20. James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, and Hongjun Zheng. Bandera: extracting finite-state models from Java source code. In Carlo Ghezzi, Mehdi Jazayeri, and Alexander L. Wolf, editors, Proc. 22nd International Conference on Software Engineering (ICSE 2000), pages 439-448. ACM, 2000. URL: https://doi.org/10.1145/337180.337234.
  21. Frank S. de Boer, Marcello Bonsangue, Einar Broch Johnsen, Ka I Pun, Silvia Lizeth Tapia Tarifa, and Lars Tveito. SymPaths: Symbolic execution meets partial order reduction. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich, editors, Deductive Verification - The Next 70 Years, volume 12345 of Lecture Notes in Computer Science. Springer, 2020. To appear. Google Scholar
  22. Frank S. de Boer, Dave Clarke, and Einar Broch Johnsen. A complete guide to the future. In Proc. 16th European Symposium on Programming (ESOP'07), volume 4421 of Lecture Notes in Computer Science, pages 316-330. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71316-6_22.
  23. Frank S. de Boer and Hans-Dieter A. Hiep. Axiomatic characterization of trace reachability for concurrent objects. In Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa, editors, Proc. 15th Intl. Conf. on Integrated Formal Methods (IFM 2019), volume 11918 of Lecture Notes in Computer Science, pages 157-174. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34968-4_9.
  24. Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453-457, 1975. URL: https://doi.org/10.1145/360933.360975.
  25. Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. Google Scholar
  26. Kiko Fernandez-Reyes, Dave Clarke, Ludovic Henrio, Einar Broch Johnsen, and Tobias Wrigstad. Godot: All the benefits of implicit and explicit futures. In Alastair F. Donaldson, editor, Proc. 33rd European Conference on Object-Oriented Programming (ECOOP 2019), volume 134 of LIPIcs, pages 2:1-2:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.2.
  27. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Jens Palsberg and Martín Abadi, editors, Proc. 32nd Symp. on Principles of Programming Languages (POPL 2005), pages 110-121. ACM, 2005. URL: https://doi.org/10.1145/1040305.1040315.
  28. Maurizio Gabbrielli and Simone Martini. Programming Languages: Principles and Paradigms. Springer, 2010. URL: https://doi.org/10.1007/978-1-84882-914-5.
  29. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, 1996. URL: https://doi.org/10.1007/3-540-60761-7.
  30. Patrice Godefroid. Model checking for programming languages using Verisoft. In Peter Lee, Fritz Henglein, and Neil D. Jones, editors, Proc. 24th Symp. on Principles of Programming Languages (POPL 1997), pages 174-186. ACM, 1997. URL: https://doi.org/10.1145/263699.263717.
  31. Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing. In Vivek Sarkar and Mary W. Hall, editors, Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'05), pages 213-223. ACM, 2005. URL: https://doi.org/10.1145/1065010.1065036.
  32. Gerard J. Holzmann and Margaret H. Smith. A practical method for verifying event-driven software. In Barry W. Boehm, David Garlan, and Jeff Kramer, editors, Proc. International Conference on Software Engineering (ICSE 1999), pages 597-607. ACM, 1999. URL: https://doi.org/10.1145/302405.302710.
  33. Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, and Martin Steffen. ABS: A core language for abstract behavioral specification. In Bernhard Aichernig, Frank S. de Boer, and Marcello M. Bonsangue, editors, Proc. 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), volume 6957 of Lecture Notes in Computer Science, pages 142-164. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25271-6_8.
  34. Shmuel Katz and Doron A. Peled. An efficient verification method for parallel and distributed programs. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 489-507. Springer, 1988. URL: https://doi.org/10.1007/BFb0013032.
  35. Antoni W. Mazurkiewicz. Trace theory. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advances in Petri Nets 1986, volume 255 of Lecture Notes in Computer Science, pages 279-324. Springer, 1987. URL: https://doi.org/10.1007/3-540-17906-2_30.
  36. Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, and David L. Dill. CMC: A pragmatic approach to model checking real code. In David E. Culler and Peter Druschel, editors, Proc. 5th Symposium on Operating System Design and Implementation (OSDI 2002). USENIX Association, 2002. URL: http://www.usenix.org/events/osdi02/tech/musuvathi.html.
  37. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In Richard Draves and Robbert van Renesse, editors, Proc. 8th Symposium on Operating Systems Design and Implementation (OSDI 2008), pages 267-280. USENIX Association, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/musuvathi/musuvathi.pdf.
  38. Kedar S. Namjoshi and Robert P. Kurshan. Syntactic program transformations for automatic abstraction. In E. Allen Emerson and A. Prasad Sistla, editors, Proc. 12th International Conference on Computer Aided Verification (CAV 2000), volume 1855 of Lecture Notes in Computer Science, pages 435-449. Springer, 2000. URL: https://doi.org/10.1007/10722167_33.
  39. Doron A. Peled. All from one, one for all: on model checking using representatives. In Costas Courcoubetis, editor, Proc. 5th International Conference on Computer Aided Verification (CAV'93), volume 697 of Lecture Notes in Computer Science, pages 409-423. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_34.
  40. Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. TransDPOR: A novel dynamic partial-order reduction technique for testing actor programs. In Holger Giese and Grigore Rosu, editors, Proc. Formal Techniques for Distributed Systems (FORTE/FMOODS 2012), volume 7273 of Lecture Notes in Computer Science, pages 219-234. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30793-5_14.
  41. Lars Tveito, Einar Broch Johnsen, and Rudolf Schlatte. ExoDPOR: Exogenous stateless model checking. Submitted for publication, 2020. Google Scholar
  42. Lars Tveito, Einar Broch Johnsen, and Rudolf Schlatte. Global reproducibility through local control for distributed active objects. In Heike Wehrheim and Jordi Cabot, editors, Proc. 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020), volume 12076 of Lecture Notes in Computer Science, pages 140-160. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45234-6_7.
  43. Antti Valmari. Stubborn sets for reduced state space generation. In Grzegorz Rozenberg, editor, Proc. 10th International Conference on Applications and Theory of Petri Nets, volume 483 of Lecture Notes in Computer Science, pages 491-515. Springer, 1989. URL: https://doi.org/10.1007/3-540-53863-1_36.
  44. Willem Visser, Klaus Havelund, Guillaume P. Brat, Seungjoon Park, and Flavio Lerda. Model checking programs. Autom. Softw. Eng., 10(2):203-232, 2003. URL: https://doi.org/10.1023/A:1022920129859.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact