Optimized execution of deterministic blocks in java PathFinder

Marcelo D'Amorim, Ahmed Sobeih, Darko Marinov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 Java 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 reduces execution time of deterministic blocks in JPF. JPF is written in Java as 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 a specific execution dynamically depends on. We evaluate mixed execution on six programs that use JPF for generating tests for data structures and on one case study for verifying a network protocol. The results show that mixed execution can improve the overall time for state exploration up to 36.98%, while improving the execution time of deterministic blocks up to 69.15%. Although we present mixed execution in the context of JPF and Java, it generalizes to any model checker that uses a special state representation.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings
PublisherSpringer
Pages549-567
Number of pages19
ISBN (Print)3540474609, 9783540474609
DOIs
StatePublished - 2006
Event8th International Conference on Formal Engineering Methods, ICFEM 2006 - Macao, China
Duration: Nov 1 2006Nov 3 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4260 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Conference on Formal Engineering Methods, ICFEM 2006
Country/TerritoryChina
CityMacao
Period11/1/0611/3/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Optimized execution of deterministic blocks in java PathFinder'. Together they form a unique fingerprint.

Cite this