wiki:projects/net-iocache

net-iocache

A JPF extension for model checking networked programs, by Watcharin Leungwattanakit and Cyrille Artho.

Note: This page is about net-iocache for JPF-6. For the most up-to-date version (for JPF-7), please look at https://bitbucket.org/cyrille.artho/net-iocache.

For any information or to report problems, please contact:

Watcharin Leungwattanakit: watcharin@…


Note: The documentation below refers to the new version, to be used with the current distribution of Java PathFinder from this page. To use a pre-built release, which works against JPF v4 from http://javapathfinder.sourceforge.net, go to the archive page containing the previous version: projects/net-iocache-v4

What is net-iocache?

Net-iocache is a Java PathFinder extension for verifying networked applications. JPF executes one of the processes in an application, whereas the others run on the standard Java virtual machine. Net-iocache captures inputs/outputs of the target program and replays them when the program needs again after backtracking. The algorithm to be run in net-iocache is presented in

  • C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, M. Yamamoto. Cache-Based Model Checking of Networked Applications: From Linear to Branching Time. ASE 2009, November 2009, Auckland, New Zealand.
  • C. Artho, W. Leungwattanakit, M. Hagiya, and Y. Tanabe. Efficient model checking of networked applications. In Proc. TOOLS EUROPE 2008, volume 19 of LNBIP, pages 22–40, Zurich, Switzerland, 2008. Springer.

Currently, programs are assumed to be either running as a server, accepting connections from several clients, or as a client, connecting to one server. The algorithm has been tested for depth-first search. Other search types, and other types of protocols (such as peer-to-peer) are not supported yet.

How to download.

You can obtain the source code of the extension using Mecurial (hg):

hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-net-iocache 

The new version comes with a jpf.properties file for configuration with the new version of JPF, and automatically generates a ~/.jpf/site.properties file when the project is built with Apache Ant. The generated file should work if you have checked out jpf-net-iocache as a subdirectory of the overall jpf repository, with jpf-core being another subdirectory. For example, JPF resides in project/jpf-core, the extension in project/jpf-net-iocache. Please refer to the README file for details.

How to build.

You can either build Java PathFinder from the command line with Ant, or from within Eclipse. To compile the jpf-net-iocache project, we recommend building sources with Apache Ant since it will automatically check and generate file site.properties if necessary.

To build with Ant, switch to the directory where the jpf-net-iocache extension is located (where this file is located), and run

ant

which should compile all jpf-net-iocache sources needed to run this extension in the normal mode.

To use the checkpointing mode, you must additionally run

ant make

which compiles DMTCP, a checkpointing tool, and necessary C source files.

You can run ant clean to remove all generated files.

Running net-iocache.

Extension net-iocache can run in two modes: normal mode and checkpointing mode.

Normal Mode

If you want to verify your own program, you should set JPF_CORE to the directory you installed the jpf-core project. You then need to specify the following options to JPF to use net-iocache:

(for the normal mode)

java -jar ${JPF_CORE}/build/RunJPF.jar \
+classpath="[classpath to your application]" \
+sourcepath="[source path to your application]" \
+report.console.property_violation=error,trace \
+listener=gov.nasa.jpf.network.listener.CacheNotifier,gov.nasa.jpf.network.listener.CacheLogger \
+jpf-net-iocache.boot.peer.command="[for server:command to start client process]" \
+jpf-net-iocache.arg0="[argument 0 of the client process]" \
+jpf-net-iocache.arg1="[argument 1 of the client process]" \
...
Application [application_args]

The first argument ensures that JPF can find your application classes. The second argument (sourcepath) points to the source code of your application. If JPF finds an error in your application, the error trace with source code will be displayed. The third argument (property_violation) tells JPF to report the trace to the error it has detected; the fourth argument (listener) activates the cache. If a client is verified, jpf-net-iocache.boot.peer.command can be omitted; if a server is verified, the cache needs to know what kind of process to spawn when the server is waiting for a client to connect. You can supply arguments for the client process by adding option jpf-net-iocache.arg[n] where n is the nth argument. If you verify a client program, make sure that a server program is running before starting JPF.

(for the checkpointing mode: CBUILD_DIR is directory c-build in this extension.)

java -Djava.library.path=${CBUILD_DIR} -jar ${JPF_CORE}/build/RunJPF.jar \
+classpath="[classpath to your application]" \
+sourcepath="[source path to your application]" \
+report.console.property_violation=error,trace \
+listener=gov.nasa.jpf.network.listener.VirtualizationCacheNotifier,gov.nasa.jpf.network.listener.VirtualizationCacheLogger \
+jpf-net-iocache.virtual.mode=true \
+jpf-net-iocache.checkpoint.dir=${CHKPNT_DIR} \
+jpf-net-iocache.lazy.connect=false \
+jpf-net-iocache.dmtcp.enabled=true \
+jpf-net-iocache.sut_private_port=${SUT_PORT} \
...
Application [application_args]

Properties jpf-net-iocache.boot.peer.command and jpf-net-iocache.arg[n] have no effect in the checkpointing mode.

An alternative way to execute JPF with several options is to create an application property file. From the sample command above, you can create property file like this:

(for the normal mode)

target = [Application]
target_args = [application_args]
classpath = [classpath to your application]
sourcepath = [source path to your application]
report.console.property_violation = error,trace
listener = gov.nasa.jpf.network.listener.CacheNotifier,gov.nasa.jpf.network.listener.CacheLogger
jpf-net-iocache.boot.peer.command = [for server:command to start client process]
jpf-net-iocache.arg0 = [argument 0 of the client process]
jpf-net-iocache.arg1 = [argument 1 of the client process]
...

(for the checkpointing mode)

target = [Application]
target_args = [application_args]
classpath = [classpath to your application]
sourcepath = [source path to your application]
report.console.property_violation = error,trace
listener = gov.nasa.jpf.network.listener.VirtualizationCacheNotifier,gov.nasa.jpf.network.listener.VirtualizationCacheLogger
jpf-net-iocache.virtual.mode = true
jpf-net-iocache.checkpoint.dir = [CHKPNT_DIR]
jpf-net-iocache.lazy.connect = false
jpf-net-iocache.dmtcp.enabled = true
jpf-net-iocache.sut_private_port = [SUT_PORT]
...

Suppose that you save the above property file as myapplication.jpf, the command starting JPF becomes like this:

(for the normal mode)

java -jar ${JPF_CORE}/build/RunJPF.jar myapplication.jpf

(for the checkpointing mode)

java -Djava.library.path=${CBUILD_DIR} -jar ${JPF_CORE}/build/RunJPF.jar myapplication.jpf

For other (optional) arguments to net-iocache, see below ("Other options/tuning"). For examples of start-up scripts, see the scripts ending with -mc.sh in directory bin. An example .jpf file is src/examples/gov/nasa/jpf/network/chat/ChatServerBug.jpf. Other examples will be converted to jpf files as well.

This project comes with a default property file, jpf.properties. It contains default JPF options whose namespace is "jpf-net-iocache". The default options usually need not be modified. If you want to specify additional options for your program, please add them into your application property file or the command line starting JPF. Please see how JPF properties are applied from Configuring JPF.

Checkpointing Mode

To use net-iocache in the checkpointing mode, make sure that:

  1. The value of /proc/sys/vm/vdso_enabled is zero. If not, make it zero by command

echo 0 | sudo tee -a /proc/sys/vm/vdso_enabled.

  1. Set the location to store checkpoints to variable CHKPNT_DIR. An example command to set its value is

export CHKPNT_DIR="${PROJ_TOP}/tmp-secure-server".

  1. Set the port number that the extension will use to receive extra information from the checkpointing tool to variable SUT_PORT. For example,

export SUT_PORT="8791"

The starting order of each process in a system is important. There are at least four processes we must consider: DMTCP coordinator, a proxy process, a client and a server.

  • The DMTCP coordinator is started by command:

${DMTCP_COORDINATOR} --ckptdir ${CHKPNT_DIR} --background

where DMTCP_COORDINATOR points to dmtcp_coordinator in directory tools/dmtcp/bin, and CHKPNT_DIR is the directory for storing checkpoints you have set before.

  • The proxy process is started by command:

${DMTCP_CHECKPOINT} c-build/proxy &

where DMTCP_CHECKPOINT points to dmtcp_checkpoint in directory tools/dmtcp/bin. Note that you must run the proxy process in the background.

If your process under test is a client, start the processes in the following order: DMTCP coordinator -> client (JPF) -> server -> proxy. If your process under test is a server, start the processes in this order: DMTCP coordinator -> server (JPF) -> proxy -> client. See normal mode for how to run JPF with this extension. You also need to add option -Djava.library.path=c-build when executing java. It is probably easier to start verification by a shell script. For examples of start-up scripts in the checkpointing mode, see the scripts ending with -dmtcp.sh in directory bin.

Logging

You can see log messages from jpf-net-iocache by setting option log.info or log.fine depending on which log level you are interested. Class CacheLayer logs messages on level "info". They include the number of bytes the cache gets from polling and the standard output of the client peer program. To see such messages, please set option log.info to gov.nasa.jpf.network.cache.CacheLayer. Class CacheLogger logs the order of search states that JPF has traversed, so users can see how the state space is explored. To see such messages, please set option log.fine to gov.nasa.jpf.network.cache.listener.

Running the examples.

You can find the scripts to run the example programs in directory "bin". You may want to make sure that net-iocache is properly built by running

./alphabet-client-mc.sh 2 1

which verifies the alphabet client with two threads inside JPF and generates the alphabet server process to handle the client threads.

The scripts that end with "-mc" start JPF verifying an example program and the peer process of the program.

You can write your own script by using one of the provided scripts as a template. All "mc" scripts include file "env.sh", which initializes shell variables used in most scripts to default values. The meaning of each variable is described below.

  • JPF_HOME: JPF base directory (default: the parent directory of jpf-net-iocache)
  • JPF_CORE: jpf-core base directory (default: directory jpf-core under JPF_HOME)
  • SRC_DIR: jpf-net-iocache base directory (default: directory jpf-net-iocache under JPF_HOME)
  • LIB_DIR: directory containing necessary jar files
  • BIN_DIR: directory containing the startup scripts
  • VM_ARG: This contains arguments for the Java virtual machine.
  • CLASSPATH: Classpaths that JPF needs including JPF core classes, model classes, native peer classes, and example program classes.
  • RUN_EXAMPLE_CMD: A command to start a JPF process verifying an example program. It includes default options as shown in section Running net-iocache. You can change values and add extra options by adding "+<option>=<value>" to this variable.
  • OPTION_PREFIX: The prefix of options specific to jpf-net-iocache. (default: jpf-net-iocache)

Other options/tuning.

net-iocache introduces three new options: exception.simulation, main.termination, and lazy.connect.

  • exception.simulation: If this option is set to true, calls to a network operation will result in either success or failure. Both possibilities are simulated by JPF. (Default: false)
  • main.termination: If it is true, the main thread will run solo until the end before the other threads start running. This option would improve performance of verification when the main thread does nothing but creating worker threads. (Default: true)
  • lazy.connect: If it is true, net-iocache will not open a physical connection immediately after the program calls method "connect". (Default: true)

Jar archives

The jar files at the bottom of this page contain builds against the old version of JPF (version 4) from sourceforge.net. Archives for v6 are coming out soon.

Last modified 5 years ago Last modified on 09/10/2013 12:58:38 PM

Attachments (4)

  • net-iocache.jar (39.4 KB) - added by telcontar@… 9 years ago. net-iocache extension that has to be copied to ${JPF_HOME}/extensions; tested under JPF v4.
  • net-env.jar (12.6 KB) - added by telcontar@… 9 years ago. * net-env.jar, Java model classes that have to be placed in the vm.bootclasspath, see documentation.
  • net-iocache.2.jar (41.2 KB) - added by telcontar@… 8 years ago. net-iocache extension that has to be copied to ${JPF_HOME}/extensions; tested against JPF 4 from subversion (Dec. 21 2009).
  • net-env.2.jar (9.6 KB) - added by telcontar@… 8 years ago. net-env.jar, Java model classes, to be placed in the vm.bootclasspath, see documentation; built against svn on Dec. 21 2009.

Download all attachments as: .zip