dat logo




The DF4ABS is an extension of the ABS Tool Suite with a new feature, the static deadlock and livelock analyzer. ABS, an acronym for Abstract Behavioral Specification Language, is a concurrent object-oriented modeling language with functional data-types. A complete account of ABS may be found at tools.hats-project.eu/.

The DF4ABS has been defined for a subset of ABS, called core ABS. The syntax of core ABS is specified below. As a notational convention, an overlined element corresponds to any finite sequence of such element. As usual, an element between square brackets is optional.


P  ::=    Dl { T x ; s }                                    program
                                           
Dl ::=    D  |  F  |  I  |  C                               declaration

T  ::=    V  | D < T >   |   I                              type

D  ::=    data D < V > Co [ T ]                             data type 

F  ::=    def T f [< T >] (T  x) = e                        function

I  ::=    interface I { S }                                 interface

C  ::=    class C (T x) [implements I] {Fl M}               class

Fl ::=    T x                                               field declatation

S  ::=    T m(T x)                                          method signature

M  ::=    S { T x ;  s}                                     method definition

s  ::=    skip  |  s ; s  |  x = z  |  await g              statement
      |   if e { s } else { s }  |  while e { s }  
      |   return e

z  ::=    e  |  new [local] C( e )  |  e.m(e)  |  e!m(e)      expression with side effects
      |   get e
      
e  ::=    v  |  x  |  this  |  f(e)  |  case e { p ==> e }  expression

v  ::=    null  |  Co [(v)]                                 value

p  ::=    _  |  x  |  null  |  Co [(p)]                     pattern

g  ::=    e  |  x?  |  g && g                               guard

Example: the method factorial.

    class Math implements Math {
        Int fact(Int n){
            Int m = 0 ;
            if (n==0) { m = 1 ; }
            else { 
                Fut<int> x = this!fact(n-1) ;
                await x? ; 
                Int m = x.get ; 
                m = n*m ;
            }
            return m ;
        }
    }
This is a "concurrent" implementation of the factorial function. Every recursive invocation is managed by a different thread. In particular, invoking fact with a non zero argument n, amounts to creating n parallel threads on a same object (this). No deadlock will be manifested because every thread releases the lock -- the await operation -- if it cannot produce a value.

Example 2: a simple livelock.

    class C implements C {
        C m(){
            return new C();
        }
        C n(C c){
            Fut<C> fut = c!m();
            await fut?;
            return fut.get;
        }
        C h(C b){
            Fut<C> fut = b!n(this);
            return fut.get;
        }
    }       

    { // Main
      C x = new C();
      C y = new C();
      x!h(y);
    }
Main creates two objects: x and y. The invocation of h on x with argument y gets the lock of x without releasing it (the get operation in the body of h). The invocation b!n(this) in the body of h amounts to invoking n on y (because b is replaced by y) and passing x as argument. However, this invocation is fated to cycle in the process of releasing the lock of y and aquiring it again because await fut? will never become a value.

Example 3: scheduler choice.

class C implements C {
   C m(){
	return new C();
   }
   C n(C c){
	Fut<C> fut = c!m();
	return fut.get;
   }
}

{ // Main
  C x = new C();
  C y = new C();
  x!n(y);
  y!n(x);
}
This is an example of possible run-time deadlock due to specific scheduler choices. Main creates two objects: x and y. Then the method n is invoked twice: the first time on x with argument y and the second time on y with argument x. If the scheduler decides to execute the body of n, and then the method m, everything will be fine. If the scheduler decides to execute the body of n and then serve the second invocation of n, a deadlock will be manifested because both x and y will be blocked. The tool, in a case like this, signals the deadlock, even if a run time deadlock can appear or not.

The DF4ABS tool consists of a contract inference system, which extracts contracts from ABS programs, and two deadlock analysis modules.

The web interface shows the two modules (DF4ABS/fixpoint and DF4ABS/model-check ) at work. The natural input is an ABS program.

The module DF4ABS/model-check tool detects deadlock in LAM programs, which can be written directly, or can be obtained by translation from ABS contracts.

The LAM programs must adhere to the following syntactical conditions:
  1. function names and variable names must start with a letter and contain either letters, or numbers or underscore
  2. es. function(var1,var2) is OK function_1(Var1, Var2) is NOT OK
  3. the first function definition is always the "main" of the lam and it must contain at least one argument
  4. each function is defined in a one line of the file (new line corresponds to a new function)
Here is the syntax of a lam program:
grammar Lam;


LPAREN  : '(';
RPAREN  : ')';
PLUS    : '+' | ';';
AND     : '&' | '||';
EQUALS  : '=';
ZERO    : '0';
COMMA   : ',';


WS              : (' '|'\t'|'\n'|'\r')-> skip;
ID              : CHAR (CHAR | DIGIT)* ;

fragment CHAR 	: 'a'..'z' |'A'..'Z' |'_' ;
	
fragment DIGIT	: '0'..'9';	

LINECOMENTS 	: '//' (~('\n'|'\r'))* -> skip;
	

BLOCKCOMENTS: '/*'( ~('/'|'*')|'/'~'*'|'*'~'/'|BLOCKCOMENTS)* '*/' -> skip;


program : lam (lam)*;

lam     : ID LPAREN params? RPAREN EQUALS expSum;

expSum  : expAnd (PLUS expAnd)*;

expAnd  : subExp (AND subExp)*;

subExp  : zero 
        | couple
        | funCall
        | group
        ;

group   : LPAREN expSum RPAREN;

zero    : ZERO;

couple  : LPAREN ID COMMA ID RPAREN;

funCall : ID LPAREN params? RPAREN;

params  : ID (COMMA ID)*;