.gitignore

*.aux
*.dvi
*.eps
*.log
*.pdf

emulated-socket-channel-state-transitions.gv

digraph EmulatedSocketChannelStateTransitions {
    rankdir=LR
    size="8,5"

    node [ shape = doublecircle ] Init
    node [ shape = point        ] Internal1 Internal2
    node [ shape = circle       ]

    Opened  [ label = "Opened\n (pending = t)" ]
    Pending [ label = "Pending\n (pending = t)" ]
    Connected [ label = "Connected\n (pending = f)" ]

    {
      rank = same
      Opened -> Init [ label = "open" ]
    }

    Opened    -> Internal1 [ label = "physical connect" ]
    Internal1 -> Pending   [ label = "true" ]
    Internal1 -> Connected [ label = "false" ]
    Pending   -> Internal2 [ label = "finishConnect" ]
    Internal2 -> Pending   [ label = "true" ]
    Internal2 -> Connected [ label = "false" ]
}

Makefile

RM=rm -f

LATEX=latex
DVIPDFMX=dvipdfmx
DOT=dot

SOURCES=shouichi.tex
DVI=$(SOURCES:.tex=.dvi)
PDF=$(SOURCES:.tex=.pdf)

GRAPHS=socket-channel-state-transitions.gv emulated-socket-channel-state-transitions.gv
EPS=$(GRAPHS:.gv=.eps)

all: eps pdf
	gnome-open $(PDF)

dvi: $(DVI)

pdf: $(PDF)

eps: $(EPS)

.SUFFIXES:
.SUFFIXES: .gv .eps .tex .dvi .pdf

.gv.eps:
	$(DOT) -T eps -o $@ $<
	touch *.tex

.tex.dvi:
	$(LATEX) $<
	$(LATEX) $<

.dvi.pdf:
	$(DVIPDFMX) $<

.PHONY: clean wc

clean:
	$(RM) *.dvi *.pdf *.aux *.log *.eps

wc:
	detex $(SOURCES) | wc

shouichi.tex

\documentclass[a4paper]{article}
\usepackage{graphicx}
\usepackage{amsmath, amssymb}
\usepackage{listings}
\usepackage{fancybox}
\usepackage{indentfirst}

\lstset{%
  frame={tb}
}%

\title{Emulating Non-blocking IO on Top of Blocking IO in Java PathFinder}
\author{Shouichi Kamiya}
\date{\today}

\begin{document}
\maketitle
\renewcommand{\thesection}{\Roman{section}}

\begin{abstract}
Java PathFinder (JPF) is a model checker for Java bytecode. It detects property
violation such as deadlocks or un-handled exceptions. It was open sourced by
NASA and many extensions are available. By using net-io-cache extension, JPF
supports network applications using blocking IO (java.net and java.io.)
However JPF does not support non-blocking IO (java.nio) at all. We support non-blocking
IO by emulating it using blocking IO and logical flags.
\end{abstract}

\section{Introduction}
Many applications communicate with other applications over network. They are often
implemented using threads to handle multiple connections. Because of network
communications and threads, there are two non-determinism. One is the thread execution
order and other is the order in which incoming messages arrive. In software testing,
a test code only covers one execution path and incoming message order. To ensure that
no execution order and incoming message order cause a failure, it is desirable to
model check such system.

JPF explores the all reachable state accounting for non-determinism such
as thread schedules. However JPF cannot model check networked applications.
The problem is that state space exploration involves backtracking. After
backtracking, JPF executes certain part of the application but external
process (which is not under control of JPF) cannot be synchronized with
backtracking. Backtracking might result repeated communications and that
might cause error on the external application.

Existing work called net-io-cache sloves this problem by capturing and caching
the communications between system under test (SUT) and its environment.
If the SUT tries to communicate with its environment, the communications
is physically executed. At the same time, net-io-cache captures the
communications and cache it. When backtracking, previously observed
communication data is fetched from cache and no physically communications
is executed.

Net-io-cache works for blocking IO (java.net and java.io) but does not
work for non-blocking IO (java.nio). Recent applications such as
Hadoop use non-blocking IO and it is desirable to model check such system.

\section{Motivation}
Let's say we want to implement a server. With java.net we can accept, read and
write, but the problem is that java.net IO is blocking. Then we need to
spawn a thread for each connection to handle multiple connections concurrently.
Obviously this approach is resource hungry (C10K problem). On the other hand,
with java.nio we can accept, read and write without blocking. Therefore one
thread can handle multiple connections and it consumes less resource. Recent
projects such as Hadoop uses java.nio for this reason. So model checking
applications that uses java.nio is needed.

\section{Approach}
\label{sec:approach}
We can either implement java.nio from scratch or implement java.nio on top of
net-io-cache. We can implement from scratch but it is very time consuming to
re-implement caching and backtracking functionality. Moreover, re-implementing
functionality will produce lot of code duplication. Code duplication will raise
maintenance cost. (If we modify internal caching algorithm, we need to implement
the algorithm on both blocking IO and non-blocking IO.) Therefore, we decided
to implement java.nio on top of java.net + java.io.

It is ideal if we implement and support all classes and methods in java.nio but
it is not realistic becuase java.nio package is big. So our approach is: First,
implement enough classes and methods to model check basic networked application
e.g, echo server/client. Next, decide target application and implement missing
classes and methods to model check that application. Our first target is Zookeeper.
The reason we decide our first target Zookeeper is described in Section
\ref{sec:experiment}.

\newpage
\section{Method}
We emulate java.nio on top of java.net + java.io by covering all state transitions
of java.nio. The key idea is that {\bf non-blocking IO can be emulated by blocking IO
and "logical flags".} We control the logical availability flags by using
JPF's choice generator and cover all state transitions. In this section we describe
our idea by explaining a echo client example.

A simplified echo client code is in Listing \ref{lst:simplified-echo-client}. It first
the client opens selector and socket channel. Next, registers the selector to the channel.
Then selector will return ready (connectable, readable or writable) channels if there
are. And it does the corresponding operation such as read.

\begin{lstlisting}[label=lst:simplified-echo-client, caption='Simplified Echo Client']

Selector selector = Selector.open();
SocketChannel channel = SocketChannel.open();
channel.connect(InetAddress.getLocalHost()); // may not be connected
channel.register(selector);

while (true) {
    Set redyChannels = selector.select();
    for (SocketChannel sc : redyChannels) {
        if (sc.isConnectable()) {
            sc.finishConnect();
        }
        else if (sc.isReadable()) {
            sc.read(buf);
        }
        else if (sc.isWritable()) {
            sc.write(buf);
        }
    }
}

\end{lstlisting}

\newpage
In the echo client example, we have Selector, SocketChannel and InetAddress classes
but here we concentrate on describing SocketChannel behavior. From Listing
\ref{simplified-echo-client}, state transitions of SocketChannel looks like Figure
\ref{socket-channel-state-transitions}.

\begin{figure}[htbp]
  \begin{center}
    \ovalbox{
      \includegraphics[width=120mm]{socket-channel-state-transitions.eps}
    }
  \end{center}
  \caption{SocketChannel State Transition}
  \label{fig:socket-channel-state-transitions}
\end{figure}

The interesting part is that SocketChannel transits to Pending or Connected state
from Opened state non-deterministically. To emulate this behavior, we physically
connect first and then set logical pending flag 'pending' by JPF's choice generator.
If 'pending' is true then transit to Pending state, otherwise transit to Connected state.
See Figure \ref{fig:emulated-socket-channel-state-transitions} for full emulated state
transitions. From Figure \ref{fig:socket-channel-state-transitions} and
\ref{fig:emulated-socket-channel-state-transitions}, we can see that our emulation covers
all states and transitions of SocketChannel. In the same way, we emulate other
non-deterministic transitions in java.nio.

\begin{figure}[htbp]
  \begin{center}
    \ovalbox{
      \includegraphics[width=120mm]{emulated-socket-channel-state-transitions.eps}
    }
  \end{center}
  \caption{Emulated SocketChannel State Transition}
  \label{fig:emulated-socket-channel-state-transitions}
\end{figure}

\section{Experiment}
\label{sec:experiment}
We implemented basic part of java.nio e.g. enough class/methods to model check echo
server/client. Next, like described in Section \ref{sec:approach}, we decided our first target
application to Zookeeper. Zookeeper is a centralized service for distributed
system and provides naming, distributed synchronization etc. Hadoop uses Zookeeper
internally. Typical Hadoop job takes hours and failure after long run wastes hours. So it is
desirable to model check such system.

We start from model checking small unit tests from Zookeeper and we successfully model checked
three unit tests. Next we tried to re-produce a known bug related to thread execution order.
But the problem is the unit test which causes the bug spawns more than ten threads. Normally
JPF can only handles two to three threads. As a result model checking the unit test fails
due to the out of memory error. Now we try to reducing the unit test to run it on JPF but
still couldn't.

\section{Conclusion}
Recent applications are often multi threaded and networked. For scalability, many networked
applications use non-blocking IO. On the other hand, non-determinism of thread execution
order and incomming/outcomming message order makes applications complex. It is desirable
to some how model check such applications. Currently JPF can only model check applications
with blocking IO. So We emulate non-blocking IO by using blocking IO and logical flags.
Therefore it is possible to model check applications with non-blocking IO. We already model
checked relatively small applications (e.g. small unit tests from Zookeeper) but could not
model check real applications (e.g. big unit tests from Zookeeper).

\section{What I Want To Do in Argentina :)}
Now I'm concluding my work and I expected to finish until May. So what I want to do next is
pretty different form this paper. I realized that JPF need more computation power through
this work. (JPF runs about twelve hours for a big unit test.) In addition, I'm really
interested in distributed system. So {\bf what I want to do next is distributed model checking}.

There is two existing works regarding to distributed JPF. One is that they start multiple JPF
on several machines. On each JPF it searches state space randomly. As a result, they find
error state faster. Every JPF runs independently so this is not "distributed". Another work is
truly distributed. They start multiple JPF and every JPF exchange messages and synchronize
visited state. They claim that they can find error state faster but overhead of exchanging
messages are really big and it was hard to reduce that.

What I'm thinking is to combine those works: Start multiple JPF and each JPF searches state space
randomly but synchronize state space periodically. I expect that will reduce the overhead
of exchanging messages and will find bug faster. However I don't still survey distributed model
checking and definitely need to survey before start working.

\end{document}

socket-channel-state-transitions.gv

digraph SocketChannelStateTransitions {
    rankdir=LR
    size="8,5"

    node [ shape = doublecircle ] Init
    node [ shape = circle       ]

    Init
    Opened
    Pending
    Connected

    Init    -> Opened    [ label = "open"          ]
    Opened  -> Pending   [ label = "connect"       ]
    Opened  -> Connected [ label = "connect"       ]
    Pending -> Pending   [ label = "finishConnect" ]
    Pending -> Connected [ label = "finishConnect" ]
}