The Static Deadlock Analyzer @ unibo

sda logo

The SDA_Tool 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 SDA_Tool 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 [cog] 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){
            if (n==0) { return 1 ; } 
            else { 
                Fut<int> x = this!fact(n-1) ;
                await x? ; 
                Int m = x.get ; 
                return n*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 cog 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 cog C();
      C y = new cog 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 cog C();
   }
   C n(C c){
	Fut<C> fut = c!m();
	return fut.get;
   }
}

{ // Main
  C x = new cog C();
  C y = new cog 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.