Version 1.2 of SOC has been released! (See details) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Abstract |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
SOC is a
program slicer for CSP specifications. In order to increase the precision of
program slicing, SOC uses a new data structure called Context-sensitive
Synchronized Control Flow Graph (CSCFG). Given a CSP specification, SOC
generates its associated CSCFG and produces from it two different kinds of
slices; which correspond to two different static
analyses. We present the tool's architecture, its main applications and the
results obtained from experiments conducted in order to measure the
performance of the tool.
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Motivation: Static Analysis of Concurrent Languages with Explicit Synchronization |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The Communicating
Sequential Processes (CSP) language allows us to specify complex systems
with multiple interacting processes. The study and transformation of such
systems often implies different analyses (e.g., deadlock analysis,
reliability analysis, refinement checking, etc.) which are often based on a data
structure able to represent all computations of a specification. Recently, two new static analyses for CSP have been
defined. They are based on a well-known program comprehension technique
called program slicing.
Program slicing is a
method for decomposing programs by analyzing their data and control flow.
Roughly speaking, a program slice consists of those parts of a program that
are (potentially) related with the values computed at some program point
and/or variable, referred to as a slicing criterion. Program slices are
usually computed from a Program Dependence Graph (PDG) that makes explicit
both the data and control dependences for each operation in a program.
Program dependences can be traversed backwards or forwards (from the slicing
criterion), which is known as backward or forward slicing, respectively.
Additionally, slices can be dynamic or static, depending on whether a
concrete program's input is provided or not.
Our technique allows us
to extract the part of a CSP specification that is related to a given event
(referred to as the slicing criterion) in the specification. This technique
can be very useful to debug, understand, maintain and reuse specifications;
but also as a preprocessing stage of other analyses and/or transformations in
order to reduce the complexity of the CSP specification. In particular, given
an event in a specification, our technique allows us to extract those parts
of the specification which must be executed before
the specified event (thus they are an implicit precondition); and those parts
of the specification which could, and could not, be executed before it.
Example. Consider the following CSP specification (also shown in the previous figure):
In this specification we
have three processes (STUDENT, PARENT and COLLEGE) executed in parallel and
synchronized on common events. Process STUDENT represents the three-year
academic courses of a student; process PARENT represents the parent of the
student who gives her a present when she passes a course; and process COLLEGE
represents the college who gives a prize to those students that finish
without any fail.
Now, let us assume that
we want to know what parts of the specification must be executed before the
student fails in the second year, hence, we mark event fail of process YEAR2
(thus the slicing criterion is (YEAR2, fail)). Our slicing technique
automatically extracts the slice composed by the highlighted parts (in the
figure). This is called MEB analysis. Therefore, SOC is a powerful tool for
program comprehension. Note, for instance, that in order to fail in the
second year, the student has necessarily passed the first year. But, the
parent could or could not give a present to his son (indeed if he passed the
first year) because this specification does not force the parent to give a
present to his son until he has passed the second year. This is not so
obvious from the specification, and SOC can help to understand the real
meaning of the specification.
We can additionally
be interested in knowing what parts could be executed before the same event.
This is called CEB analysis. In this case, our technique adds to the slice
the underscored parts because they could be executed (in some executions)
before the marked event. This can be useful, e.g., for debugging. If the
slicing criterion is an event that executed incorrectly (i.e., it should not
happen in the execution), then the slice produced contains all the parts of
the specification that could produce the wrong behaviour.
A third application
of our tool is program specialization. SOC is able to extract executable
slices with a program transformation applied to the generated slices. The
specialized specification contains all the necessary parts of the original
specification whose execution leads to the slicing criterion (and then, the
specialized specification finishes).
Note that, in the slices
produced by both analyses in Figure 1, the slice produced could be made
executable by replacing the removed parts by “STOP” or by “-> STOP” if
there moved expression has a prefix.
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Implementation |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Architecture SOC has been
implemented in Prolog and it has been integrated in ProB. Therefore, SOC can take advantage of ProB's
graphical features to show slices to the user. In order to be able to color
parts of the code, it has been necessary to implement the source code
positions detection; in such a way that ProB can color every subexpression
which is sliced by SOC. Apart
from the interface module for the communication with ProB, SOC has three main modules which we
describe in the following:
Graph
Generation
The usual data structure
for program slicing (the system
dependence graph) cannot be used in CSP. In contrast, it is needed
a new data structure called Context-sensitive
Synchronized Control Flow Graph (CSCFG) as described here. A CSCFG is a data structure able to finitely represent all
possible (often infinite) computations of a CSP specification. This data structure is particularly
useful to simplify a CSP specification before its static analysis. Therefore, the first task of the
slicer is to build a CSCFG. The module that generates the CSCFG from the
source program is the only module that is ProB dependent. This means that SOC could be used in other systems by
only changing the graph generation module.
Graph Compaction
The original definition
of the CSCFG is inaccurate from an implementation point of view. Therefore,
we have implemented a module that reduces the size of the CSCFG by removing
unnecessary nodes and by joining together those nodes that form paths that
the slicing algorithms must traverse in all cases. This compaction not only
reduces the size of the stored CSCFG, but it also speeds up the slicing
process due to the reduced number of nodes to be processed.
Slicing Module
This is the main module
of the tool. It is further composed of two submodules which implement the
algorithms to perform the MEB and CEB analyses on the compacted CSCFGs.
Depending on the analysis selected by the user this module extracts a
subgraph from the compacted CSCFG using either MEB or CEB. Then, it extracts
from the subgraph the part of the source code which forms the slice. If the
user has selected to produce an executable slice, then the slice is
transformed to become executable (it mainly fills gaps in the produced slice
in order to respect the syntax of the language). The final result is then
returned to ProB in such a way that ProB can either highlight the final slice
or save a new CSP executable specification in a file.
A clear advantage of SOC is that almost all the modules of
the tool are language-independent. They relay on the construction of the
CSCFG of the program. Therefore, SOC could
be easily adapted to other languages by only modifying the module that
constructs the CSCFG.
How is SOC distributed SOC has been
implemented in Prolog and it has been integrated in the system ProB, a CSP development
environment and animator for the B-method which also supports other languages
such as CSP. ProB has been implemented in Prolog and it is publicly available
at http://www.stups.uni-duesseldorf.de/ProB.
ProB enables a user to animate a specification, either interactivally or automatically.
ProB was developed using SICStus Prolog. It uses Tcl/Tk for the Graphical
User Interface (a Java version is also available) and dot/dotty from the
Graphviz package.
How to use SOC Let us consider previous
example to show how SOC can
be used to extract slices from CSP specifications. The user has two
possibilities: to edit the specification directly in the top pane or to load it
from a file (if it exists as a previously edited file).
Once the program is
loaded, the user can slice it with a process that is fully automatic.
Concretely, the user can select (with the mouse) the event or process call
she is interested in. This simple action is enough to define a slicing
criterion because the tool can automatically determine the process and the
source position of interest. In our example, the slicing criterion is event
fail of process YEAR2, as we can see in next figure.
Then, she selects command Highlight Slice from Analyse -> Slicing menu. The tool internally
generates the CSCFG of the specification (saved in a file .dot) and uses the
MEB and CEB algorithms to construct the slices. The result is shown to the
user by highlighting the part of the specification that must (respectively
could) be executed before the specified event. Next figure shows a screenshot
of ProB showing a slice of our CSP specification example w.r.t. the slicing criterion (YEAR2,fail). We can observe
highlighted in green the MEB slice and highlighted in yellow the CEB slice
which coincide with the expected results.
Finally, the user can
view the generated CSCFG opening the corresponding .dot file. In next figure,
the CSCFG generated when Analyse
-> Slice is selected is shown. The nodes of the MEB slice
are green.
Benchmarking In order to measure the
specialization capabilities of our tool, we conducted some experiments. For
each benchmark, Table 1(a) and Table 1(b) summarize the time spent to
generate the compacted CSCFG (this includes the generation plus the
compaction phases), to produce the MEB and CEB slices (since CEB analysis
uses MEB analysis, CEB's time corresponds only to the time spent after
performing the MEB analysis), and the total time. Table 1(a) shows the
results when using the fast context and Table 1(b) shows the results
associated to the precise context. Clearly, the fast context achieves a significative
time reduction.
Table 1
Benchmark time results for the FAST and PRECISE
CONTEXT
(a) Benchmark time results for the FAST CONTEXT
(b) Benchmark time
results for the PRECISE CONTEXT
Table 2
Benchmark size results for the FAST and PRECISE
CONTEXT
(a) Benchmark size
results for the FAST CONTEXT
(b) Benchmark size
results for the PRECISE CONTEXT
In order to measure the
specialization capabilities of our tool, we conducted some experiments. The
benchmarks selected for the experiments are the following:
[ATM.csp] This specification represents an
Automated Teller Machine. The slicing criterion is (Menu,getmoney),
i.e., we are interested in determining what parts of the specification must
be executed before the menu option getmoney is chosen in the ATM.
[RobotControlling.csp] This example describes a game in
which four robots move in a maze. The slicing criterion is (Referee,winner2), i.e., we want to know what parts of the system
could be executed before the
second robot wins.
[Buses.csp] This example describes a bus
service with two buses running in parallel. The slicing criterion is (BUS37,pay90), i.e., we are interested in determining what could
and could not happen before the user payed at bus 37.
[Prize.csp] In this specification there are
three processes (STUDENT, PARENT and COLLEGE) executed in parallel and
synchronized on common events. Process STUDENT represents the three-year academic
courses of a student; process PARENT represents the parent of the student who
gives her a present when she passes a course; and process COLLEGE represents
the college who gives a prize to those students which finish without any fail. The slicing criterion is (YEAR2,fail),
i.e., we are interested in determining what parts of the specification must
be executed before the student fails in the second year.
[Phils.csp] This is a simple version of the
dining philosophers problem. In this example, the slicing criterion is (PHIL221,
DropFork2), i.e., we want to know what happened before the second philosopher
dropped the second fork.
[TrafficLights.csp] This specification defines two
cars driving in parallel on diferent streets. The first car can only
circulate in two streets. The second car can only circulate in a third
street. Each street has one traffic light for cars controlling. The slicing
criterion is (STREET3,park), i.e., we are interested
in determining what parts of the specification must be executed before the
second car parks on the third street.
[Processors.csp] This example describes a system
that, once connected, receives data from two machines. The slicing criterion
is (MACH1,datreq) to know what parts of the example
must be executed before the first machine requests data.
[ComplexSynchronization.csp] This specification defines five
routers working in parallel. Router i can only send messages to router i+1.
Each router can send a broadcast message to all routers. The slicing
criterion is (Process3,keep), i.e., we want to know
what parts of the system could be executed before router 3 keeps a message.
[Computers.csp] This benchmark describes a system
in which a user can surf internet and download files. The computer can
control if files are infected by virus. The slicing
criterion is (USER,consult_file), i.e., we are
interested in determining what parts of the specification must be executed
before the user consults a file.
[Highways.csp] This specification describes a net
of spanish highways. The slicing criterion is (HW6,Toledo),
i.e., we want to determine what cities must be traversed in order to reach
Toledo from the starting point.
You can find other CSP examples here.
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Download | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Here you can download the last version of SOC: The most important improvement is to avoid repeated computations. This is done by: state memorization: once a state already explored is reached the algorithm stops this computation and starts with another one; and skipping already performed computations: computations do not start from MAIN, they start
from the next non-deterministic state in the execution (this is provided by the information of the stack).
|