HTTPS SSH
= net-iocache =
A JPF extension for model checking networked programs.

----
Note: This version is for use with Java PathFinder version 7/8. To use version 6 (or get information on version 4), please use
hg update jpf6
in this repository and check the README file.
----

Contributors:

Watcharin Leungwattanakit
Cyrille Artho
David Amar
Shouichi Kamiya
Richard Potter
Franz Weitl
Paul-Francois Jeau

For any information or to report problems, please contact:

Cyrille Artho: artho@kth.se

== What is net-iocache? ==

Net-iocache is a Java Pathfinder extension for verifying networked applications. JPF executes one of the processes as system under test (SUT), whereas the remote peers run on the standard Java virtual machine. Net-iocache captures network IO of the SUT and replays received messages after backtracking. The overall approach is presented in the short paper

 * C. Artho, W. Leungwattanakit, M. Hagiya, E. Platon, Y. Tanabe, M. Yamamoto. Cache-based Model Checking of Networked Software. DNSA 2010, December 2010, Hiroshima, Japan. 

Details of the caching algorithm of net-iocache are described, for instance, 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.

== Getting and installing the appropriate version of JPF ==

This version of net-iocache is tested for JPF v7. We assume that jpf-core v7 is available in ~/project/jpf-core. Its latest revision can be obtained and built by changing to the directory ~/project

{{{
cd ~/project
}}}

and executing the two commands

{{{
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
ant
}}}

Details on installing JPF are available on 

* http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start


== How to download net-iocache ==

You can obtain the source code of the extension net-iocache using Mercurial (hg). 
Execute the command 
{{{
hg clone https://bitbucket.org/cyrille.artho/net-iocache
}}}

Authorized users may obtain the current developer snapshot from

{{{
hg clone ssh://hg@bitbucket.org/cyrille.artho/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.


== Testing the setup of net-iocache ==

To check, whether jpf-net-iocache has been built correctly, run the unit tests and prepared test cases by executing

  `ant run-unit-tests`
  `bin/regression-tests.sh`

in the jpf-net-iocache directory. All unit tests and test cases should pass. Detailed test results are logged in the directories

  tests       (regression test results)
  build/tests (unit test results)

Output files created by unit and regression tests can be removed by executing

  `ant clean-logs`

You may run a specific unit test by passing a testcase argument to run-unit-tests. E.g., 

  `ant run-nio-tests -Dtestcase=ByteBufferTest` 

runs 'ByteBufferTest', only. Similarly, you may execute any of the test cases listed in the output of 'bin/regression-tests.sh' in isolation. For instance, 

  `bin/helloworld.sh client-sut v=3`

runs jpf on the 'helloworld client' test case with 'verbosity level 3'. Run a test case such as 'bin/helloworld.sh' without arguments to see an explanation of available options.


== Running net-iocache. ==

A good starting point for own experiments may be the 'hello world' sample scenario which can be executed by the following three shell scripts:

 `bin\helloWorld.sh`           #no model checking: execute 'hello world' server and client 
                               #  using the normal jvm 
 `bin\helloWorldClient-mc.sh`  #system under test (model checking by jpf):   'hello world' client; 
                               #remote peer (normal jvm, no model checking): 'hello world' server.
 `bin\helloWorldServer-mc.sh`  #system under test (model checking by jpf):   'hello world' server; 
                               #remote peer (normal jvm, no model checking): 'hello world' client.

The java sources and .jpf files of the 'hello world' example are located in 

	\src\examples\helloWorld
							   
'hello world' runs in ''normal mode'' of net-iocache. In addition to the ''normal mode'', net-iocache supports the ''checkpointing mode''.

=== Normal 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)
{{{
#!sh

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 incl. arguments to start 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. 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.)
{{{
#!sh

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]
}}}

Property `jpf-net-iocache.boot.peer.command` has 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 incl. arguments to start 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)
{{{
#!sh

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

(for the checkpointing mode)
{{{
#!sh

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 [http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/config 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`.

2. 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"`.

3. 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 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 options `log.info`, `log.fine`, `log.finer`, and `log.finest` in the .jpf file, depending on the level of detail you are interested in. 

Class `CacheLayer` supports logging on level "info", "fine", and "finer". Logging output includes the number of bytes the cache receives from the remote peer and the standard output of the peer process. To see such messages, set option `log.info`, `log.fine`, or `log.finer` to `gov.nasa.jpf.network.cache.CacheLayer`. 

Class `CacheLogger` logs the exploration process of the state space. To see such messages, set option `log.fine`, `log.finer`, or `log.finest `to `gov.nasa.jpf.network.listener`.

Example settings:

* Example 1:

{{{
 log.info = gov.nasa.jpf.network.listener
 log.fine = 
 log.finer= gov.nasa.jpf.network.cache.CacheLayer
}}}

Do not omit line 2. This logs summary information about the state space traversal, only, but detailed information on network IO and changes to data structures of net-iocache. 

* Example 2:

{{{
 log.info = 
 log.fine = 
 log.finer= gov.nasa.jpf.network.cache.CacheLayer;gov.nasa.jpf.network.listener
}}}

Do not omit line 1 and 2. This logs detailed information on both the state space traversal and network IO. 

== 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 [#Runningnet-iocache. 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 the following new options which may be set in the .jpf file of the SUT: 

 * `jpf-net-iocache.exception.simulation` (default: false): If this option is set to true, network operations of the SUT will result in either success or failure. Both possibilities are explored by JPF. If it is set to false, all network operations will be successful at the model level. If a network operation fails at the native level, jpf will report an exception and terminate exploring the state space of the SUT.
 
 * `jpf-net-iocache.main.termination` (default: false): If it is true, the main thread will run solo until the end, before the other threads start running. This improves the performance of verification when the main thread does nothing but creating worker threads. Make sure that this option is set to false if the main thread synchronizes with other threads, for instance, by waiting for the termination of a started thread via join(). Otherwise, jpf is likely to run into a deadlock.

 * `jpf-net-iocache.lazy.connect` (default: false): If this is set to true, net-iocache will not open a physical connection immediately after the SUT calls the method "connect" on a socket. Instead, the connection will be delayed until the first write operation. This is preferable if the remote peer (server) does   n o t   respond by sending an initial message immediately after accepting a connection. If the remote peer   d o e s   send an initial message, lazy.connect should be set to false. Otherwise, the initial message will be confused as response to the first request written out by the SUT. 

 * `jpf-net-iocache.peerResponse.maxDelayMillis` (default: 150, set to 25 in the file jpf.properties of jpf-net-iocache): This sets the time span in ms within a remote peer is expected to send his complete response after receiving a request. Moreover, if the remote peer sends a message immediately after accepting a connection, it is expected to send it within jpf-net-iocache.peerResponse.maxDelayMillis ms. Set this value sufficiently large to ensure that net-iocache recognizes and stores request-response patterns correctly. Increase this value if net-iocache keeps dropping delayed messages or associating them with the wrong requests. A value of 0 indicates infinite delay, i.e., after connecting to the remote peer and after each network output of the SUT, jpf will block (possibly infinitely) until a response from the remote peer is received.               
 
 * `jpf-net-iocache.nio.failureFirst` (default: false): configure the ORDER of choices when exploring the state space of non-blocking accept/read/write in nio. When set to false, the successful branch is explored first, i.e.,  
   * ServerSocketChannel.accept() returns a valid SocketChannel;
   * SocketChannel.read()   reads more than 0 bytes from a channel;
   * SocketChannel.write()  writes more than 0 bytes to a channel.
 When set to true, the unsuccessful branch is explored first, i.e,
   * ServerSocketChannel.accept() returns null (no pending connection request);
   * SocketChannel.read()   returns 0 bytes read (nothing is read);
   * SocketChannel.write()  returns 0 bytes written (nothing is written).
 In either case, the successful and unsuccessful branch are explored for each non-blocking accept/read/write, regardless of the value of nioFailureFirst. Be aware that in non-blocking mode, each call to accept(), read(), or write() generates an INDEPENDENT choice point, i.e., the state space grows exponentially in the number of accept/read/write method calls. Hence the following code results in a hugh (untractable) state space:  
   someServerSocketChannel.configureBlocking(false);
   SocketChannel ch=null; int i=0;
   while(ch==null) {ch = someServerSocketChannel.accept(); i++;}
 In contrast to non-blocking mode, in blocking mode accept(), read(), and write() are assumed to be always successful unless jpf-net-iocache.exception.simulation is set to true.
 
 * Further parameters for configuring net-iocache are available. Please see comments in file
   
     jpf.properties
	
   in the jpf-net-iocache top directory.
 
 == JPF Eclipse Plugin ==
  When using the JPF plugin to execute net-iocache jpf files, we recommend to enable asseration checking in the host VM: Window -> Preferences ->  JPF Preferences -> JPF's Host VM Arguments: -ea