Trustworthy Computing Laboratory (TwCL)
Iran University of Science and Technology

 

 

DSCMC

Distributed Stateless Code Model Checker

 


Quick access: What is DSCMC Tool? How to use DSCMC? How to obtain DSCMC?

 

 

DSCMC Tool: Distributed Stateless Code Model Checker
Developed in: TWcL

o   What is DSCMC Tool?

DSCMC is a stateless code model checker for systematic testing of concurrent programs under specific input. It has been developed using the Actor model and written in Erlang, which is an actor-based programming language. This tool has many different features suited to verify concurrent programs.

The required tasks of stateless model checking are dispatched among DSCMCs actors running in parallel. The tool executes programs in their real runtime environment under the control of its special scheduler. The scheduler controls nondeterministic execution of threads. DSCMC accepts all possible interleavings under strong fairness.

o   How to use DSCMC?

DSCMC can be used in two different configurations; in the first configuration, it is able to detect deadlocks, livelocks, and data races. Most importantly, it can check LTL formulae. The second configuration is dedicated to the verification of information flow security, in which it can detect livelocks and deadlocks as well. In order to use the tool, the program code must be instrumented. Code instrumentation is performed in a different way for each configuration. DSCMC always initiates the model checking process from a central node. Then workload is distributed among available computational nodes. The model checking process is shown in Fig. 1.

 

 

Fig 1. The process of model checking in DSCMC

 

 

 

Fig. 2 shows the DSCMC architecture. As mentioned above, program code must be instrumented before starting model checking. Code is instrumented so that the state of the executing program can be monitored, and the program can communicate with DSCMC. Thereafter, the program is compiled into an executable and the model checker runs the executable repeatedly under the control of its scheduler until all relevant interleavings among the threads are explored. Before executing any operation that might have effects on the other threads, the instrumented program sends a request to the program side interface (Pi). It delivers the message to the scheduler. The scheduler can block the requester by postponing a reply. Pi is a controller at the program side and regulates communications between the program and DSCMCs actors. In fact, this interface is an actor that formats the information related to a program state as a message and sends it to the tool side interface (Ti) actor. All requests for communication with the scheduler and other components of DSCMC are sent via Pi to Ti. Ti delivers messages received from Pi to the other actors according to their headers and contents. This architecture makes it possible to use the tool for verifying programs written in different programming languages. That is to say, the tool is able to support various programming languages.

Note: Currently, code is manually instrumented in DSCMC.

 

 

Fig. 2. The architecture of DSCMC

 

 

 

DSCMC has been implemented by using Erlang so you need Erlang R13B03 (Eshell V5.7.4) or higher. It has been tested under Linux systems. Currently, it supports C and the Pthread library on Linux. In this regard, the program side interface has been written as the library, nodec.h, which should be inserted in the user code during the instrumentation phase. A similar library can be implemented for any arbitrary programming language (by employing the Erlang interoperability mechanism). Therefore you can instrument your code using a suitable library. The code must be instrumented such that it can interact with DSCMC in the expected manner.

1.      After code instrumentation, you must compile it with the following command:

gcc -o cclient1 -I/usr/lib/erlang/lib/erl_interface-3.6.4/include -L/usr/lib/erlang/lib/erl_interface3.6.4/lib deadlock01.c -lerl_interface lei lsocket lnsl pthread

2.      You should prepare a configuration file for each available computational node in your distributed environment. Each node uses this file for finding the number of available computational nodes in the system, names and IP addresses of the other nodes, the number of threads in the program under test, and so on. In Fig. 3, two samples of the configuration files are shown. In a configuration file, field local_node_name specifies the name of the local node where the current node is (this name differs on each node). The field prog_node_name usually does not need to be changed. The field number_of_nodes determines the number of available computational nodes. Field dis_node_name contains the node names. IP addresses of the nodes should be written in field hosts. Field localhost shows the IP address of the local node. The number of existing threads in the program (including the main thread) should be written in the field number_of_threads. This number must be accurate. The field number_of_steps denotes the maximum number of the execution steps after which the user expects the program to come to an end. The model checker stops if an execution exceeds this bound, and reports a warning to the user. Using this mechanism, the tool is able to detect livelocks. You should prepare such a file for each computational node in your system.

 

 

Fig. 3. Samples of the configuration file

 

 

 

3.      In the next step, you should start an Erlang node as follows:

erl -name e1@10.0.2.15 -setcookie secretcookie1

where e1@10.0.2.15 is the name of the local node (i.e. local_node_name in the configuration file). Thereafter, in order to use DSCMC in a desired configuration, you should enter the related commands shown in Fig. 4 in the created Erlang shell.

 

 

Fig. 4. Calling required functions to start DSCMC

 

 

o   How to Obtain DSCMC?

To obtain the DSCMC executable, please contact by email:

o   Dr. Mohammad Abdollahi Azgomi: azgomi@iust.ac.ir, or

o   Ms. Elaheh Ghassabani: ghasabani@comp.iust.ac.ir