Resource Analysis with SRA

General Overview

We prototype a static analysis technique that computes upper bounds of virtual machine usages in a dialect of ABS, called vml, whose syntax will be covered by the examples in this tutorial, with explicit acquire and release operations of virtual machines. In our language it is possible to delegate other (ad-hoc or third party) concurrent code to release virtual machines (by passing them as arguments of invocations). Our technique is modular and consists of (i) a type system associating programs with behavioural types that records relevant information for resource usage (creations, releases, and concurrent operations), (ii) a translation function that takes behavioural types and return cost equations. It is integrated with the solver CoFloCo that given the cost equations produces the result.

Resource Analysis

In this section we present how to compute the cost of a vml program in term of virtual machine usage.

First, select Resource Analysis (SRA) from the pull-down menu at the top of the window on the center-left. The parameters of the selected analysis are automatically set, so there is nothing to be configured in the Settings section in the top-left corner.

As an example, open the program doubleRelease.vml :

/* DOUBLE RELEASE */
Int doubleRelease(VM x, VM y) {
  release x; release y;
  return 0 ;
}

Int user1() {
  VM x ; VM y ; Fut<Int> f ;
  x = new VM() ; y = new VM();
  f = this!doubleRelease(x, y);
  Int a = f.get ; return 0 ; 
}

{
  Fut<Int> fuser1 = this!user1();
  Int a = fuser1.get;
}

Let us analyze the program. Click on Run to perform the analysis.

The output of the analysis is shown in three tabs of the console, which are generated by the tool:

• Types contains the behavioural types generated for the input program
• Equations contains the cost equations resulted by the translation of the behavioural types
• UBs which is the overall output and shows the upper bounds. For the doubleRelease.vml we get:

### Partitioned upper bound of main(MAINVM):
* 2
 if []

### Partitioned upper bound of doubleRelease012net(THISVM,X,Y):
* -2
 if [THISVM=1,X=1,Y=1]
* -1
 if [THISVM=1,X=1,Y>=2]
 or [THISVM=1,Y=1,X>=2]
* 0
 if [THISVM=1,X>=2,Y>=2]
 or [THISVM=3]

### Partitioned upper bound of user10net(THISVM):
* 0
 if [3>=THISVM,THISVM>=1]

### Partitioned upper bound of doubleRelease012peak(THISVM,X,Y):
* 0
 if [X=1,Y=1,2>=THISVM]
* 0
 if [X=1,2>=THISVM,Y>=2]
 or [Y=1,2>=THISVM,X>=2]
 or [X=1,2>=THISVM,0>=Y]
* 0
 if [2>=THISVM,X>=2,Y>=2]
 or [2>=THISVM,0>=Y,X>=2]
 or [3>=THISVM,0>=X]
 or [THISVM=3,X>=1]

### Partitioned upper bound of user10peak(THISVM):
* 0
 if [THISVM=3]
* 2
 if [2>=THISVM]