Vector-clock based partial order reduction for JPF
- 11 February 2014
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGSOFT Software Engineering Notes
- Vol. 39 (1), 1-5
- https://doi.org/10.1145/2557833.2560581
Abstract
Java Pathfinder (JPF) employs a dynamic partial order reduction based on sharing and state hashing to reduce the schedules in concurrent systems. That partial order reduction is believed to be complete in the new version of JPF using search global IDs (SGOIDs) but does miss behaviors when SGOIDs are not employed. More importantly, it is not clear how such a dynamic partial order reduction, with or without SGOIDs, compares to other dynamic partial order reductions based on persistent sets, sleep sets, or clock vectors. In order to understand JPF's native dynamic partial order reduction better, this paper discusses an implementation of Flanagan and Goidefroid's clock vector partial order reduction in JPF. Then, the performance of JPF's native dynamic partial order reduction and the clock vector partial order reduction in JPF using SGOIDs will be compared in an effort to understand JPF's dynamic partial order reduction more fully. It was discovered that a clock vector POR always performs better in terms of runtime on the benchmarks chosen, and sometimes even better in terms of memory.This publication has 5 references indexed in Scilit:
- Hardness for Explicit State Software Model Checking BenchmarksPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2007
- Dynamic partial-order reduction for model checking softwarePublished by Association for Computing Machinery (ACM) ,2005
- Implementing LTL model checking with net unfoldingsLecture Notes in Computer Science, 2001
- Static partial order reductionPublished by Springer Science and Business Media LLC ,1998
- Partial-Order Methods for the Verification of Concurrent SystemsLecture Notes in Computer Science, 1996