The CSP's Slicer SOC
  newVersion 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.

SOC

Example. Consider the following CSP specification (also shown in the previous figure):

MAIN = (STUDENT || PARENT) || COLLEGE

STUDENT = year1 -> (pass -> YEAR2 [] -> STUDENT)

YEAR2 = year2 -> (pass -> YEAR3 [] fail -> YEAR2)

YEAR3 = year3 -> (pass -> graduate -> STOP [] fail -> YEAR3)

PARENT = pass -> present -> pass -> present -> pass -> present -> STOP

COLLEGE = fail -> STOP [] pass -> C1

C1 = fail -> STOP [] pass -> C2

C2 = fail -> STOP [] pass -> prize -> STOP

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

 
 

bola Architecture

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.

bola 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.

bola 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).

SOC

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.

SOC

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.

SOC

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.

CSCFG

bola 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 2(a) and Table 2(b) summarize the size of all objects participating in the slicing process for both the fast and the precise contexts respectively: Column Original CSCFG shows the size of the CSCFG of the original program. Column Com CSCFG shows the size of the compacted CSCFG. Column (%) shows the percentage of the compacted CSCFG' size with respect to the original CSCFG. Finally, columns MEB Slice and CEB Slice show respectively the size of the MEB and CEB CSCFG' slices. Clearly, CEB slices are always equal or greater than their MEB counterparts 4. The CSCFG compaction technique shows to be very useful. Experiments show that the size of the original specification is substantially reduced using this technique. The size of both MEB and CEB slices obviously depends on the slicing criterion selected. Table 2(a) and Table 2(b) compare both slices with respect to the same criterion and, therefore, they give an idea of the difference between them.

Table 1

Benchmark time results for the FAST and PRECISE CONTEXT

 

(a) Benchmark time results for the FAST CONTEXT

 

Benchmark

CSCFG

MEB

CEB

Total

ATM.csp

805 ms.

36 ms.

67 ms.

908 ms.

Robot Controlling .csp

277 ms.

39 ms.

21 ms.

337 ms.

Buses.csp

29 ms.

2 ms.

1 ms.

32 ms.

Prize.csp

55 ms.

35 ms.

10 ms.

100 ms.

Phils.csp

72 ms.

12 ms.

4 ms.

88 ms.

TrafficLights.csp

103 ms.

20 ms.

12 ms.

135 ms.

Processors.csp

10 ms.

4 ms.

2 ms.

16 ms.

ComplexSynchronization.csp

212 ms.

264 ms.

38 ms.

514 ms.

Computers.csp

23 ms.

6 ms.

1 ms.

30 ms.

Highways.csp

11452 ms.

100 ms.

30 ms.

11582 ms.

 

(b) Benchmark time results for the PRECISE CONTEXT

Benchmark

CSCFG

MEB

CEB

Total

ATM.csp

10632 ms.

190 ms.

272 ms.

11094 ms.

Robot Controlling .csp

2603 ms.

413 ms.

169 ms.

3185 ms.

Buses.csp

25 ms.

1 ms.

0 ms.

26 ms.

Prize.csp

352 ms.

317 ms.

79 ms.

748 ms.

Phils.csp

96 ms.

12 ms.

8 ms.

116 ms.

TrafficLights.csp

2109 ms.

1678 ms.

416 ms.

4203 ms.

Processors.csp

15 ms.

2 ms.

5 ms.

22 ms.

ComplexSynchronization.csp

23912 ms.

552 ms.

174 ms.

24638 ms.

Computers.csp

51 ms.

4 ms.

6 ms.

61 ms.

Highways.csp

58254 ms.

1846 ms.

2086 ms.

62186 ms.

   

Table 2

Benchmark size results for the FAST and PRECISE CONTEXT

 

(a) Benchmark size results for the FAST CONTEXT  

Benchmark

Original CSCFG

Compacted CSCFG

(%)

MEB Slice

CEB Slice

ATM.csp

156 nodes

99 nodes

63,46 %

32 nodes

45 nodes

RobotControlling.csp

337 nodes

121 nodes

35,91 %

22 nodes

109 nodes

Buses.csp

20 nodes

20 nodes

100 %

11 nodes

11 nodes

Prize.csp

70 nodes

52 nodes

74,29 %

25 nodes

42 nodes

Phils.csp

181 nodes

57 nodes

31,49 %

9 nodes

39 nodes

TrafficLights.csp

113 nodes

79 nodes

69,91 %

7 nodes

60 nodes

Processors.csp

30 nodes

15 nodes

50 %

8 nodes

9 nodes

ComplexSynchronization.csp

103 nodes

69 nodes

66,99 %

37 nodes

69 nodes

Computers.csp

53 nodes

34 nodes

64,15 %

18 nodes

29 nodes

Highways.csp

103 nodes

62 nodes

60,19 %

41 nodes

48 nodes

 

(b) Benchmark size results for the PRECISE CONTEXT  

Benchmark

Original CSCFG

Compacted CSCFG

(%)

MEB Slice

CEB Slice

ATM.csp

267 nodes

165 nodes

61,8 %

52 nodes

59 nodes

RobotControlling.csp

1139 nodes

393 nodes

34,5 %

58 nodes

369 nodes

Buses.csp

22 nodes

20 nodes

90,91 %

11 nodes

11 nodes

Prize.csp

248 nodes

178 nodes

71,77 %

15 nodes

47 nodes

Phils.csp

251 nodes

56 nodes

22,31 %

9 nodes

39 nodes

TrafficLights.csp

434 nodes

267 nodes

61,52 %

7 nodes

217 nodes

Processors.csp

37 nodes

19 nodes

51,35 %

8 nodes

14 nodes

ComplexSynchronization.csp

196 nodes

131 nodes

66,84 %

18 nodes

96 nodes

Computers.csp

109 nodes

72 nodes

66,06 %

16 nodes

67 nodes

Highways.csp

503 nodes

275 nodes

54,67 %

47 nodes

273 nodes

In order to measure the specialization capabilities of our tool, we conducted some experiments. The benchmarks selected for the experiments are the following:

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  [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.

ola  You can find other CSP examples here.

Download a paper describing SOC
hoja Download a paper describing MEB and CEB analyses
hoja Download a paper describing a Semantics to generate the CSCFG
 
  Download  
 

Here you can download the last version of SOC:
This new version implements the algorithm described in this Technical Report. However, in the implementation the algorithm is much more complex because it contains some improvements that significantly speed up the CSCFG construction.

The most important improvement is to avoid repeated computations. This is done by:

ola state memorization: once a state already explored is reached the algorithm stops this computation and starts with another one; and

ola 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).


SOC
STAR SOC (10-01-2010 release) Download
STAR SOC (12-05-2009 release) Download
STAR SOC (05-11-2008 release) Download
STAR SOC Modules Source Code Download
STAR Check the lattest stable version at ProB Go to