Withdraw
Loading…
Optimized Execution of Deterministic Blocks in Java PathFinder
d'Amorim, Marcelo; Sobeih, Ahmed A.; Marinov, Darko
Loading…
Permalink
https://hdl.handle.net/2142/11211
Description
- Title
- Optimized Execution of Deterministic Blocks in Java PathFinder
- Author(s)
- d'Amorim, Marcelo
- Sobeih, Ahmed A.
- Marinov, Darko
- Issue Date
- 2006-06
- Keyword(s)
- Java PathFinder
- optimized execution
- computer science
- Abstract
- Java PathFinder (JPF) is an explicit-state model checker for Java programs. It explores all executions that a given program can have due to different thread interleavings and nondeterministic choices. JPF implements a backtracking Java Virtual Machine (JVM) that executes bytecodes using a special representation of JVM states. This special representation enables JPF to quickly store, restore, and compare states; it is crucial for making the overall state exploration efficient. However, this special representation creates overhead for each execution, even execution of deterministic blocks that have no thread interleavings or nondeterministic choices. We propose mixed execution, a technique that improves execution time of deterministic blocks in JPF. Our technique leverages the fact that JPF is written in Java: JPF is a special JVM that runs on top of a regular, host JVM. Mixed execution works by translating the state between the special JPF representation and the host JVM representation. We also present lazy translation, an optimization that speeds up mixed execution by translating only the parts of the state that an execution dynamically depends on. We evaluate mixed execution on six subject programs that use JPF for generating tests for data structures and on one case study for verifying a network protocol. The experimental results show that mixed execution can improve the overall state exploration time up to 36.98%, while improving the execution time of deterministic blocks up to 69.15%.
- Type of Resource
- text
- Permalink
- http://hdl.handle.net/2142/11211
- Copyright and License Information
- You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Owning Collections
Manage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…