Resource Analysis Demo

Introduction

The analysis of resource usage in a program is of great interest because an accurate assessment could reduce energy consumption and allocation costs. These two criteria are even more important today, in modern architectures like mobile devices or cloud computing, where resources, such as virtual machines, have hourly or monthly rates.

To the best of our knowledge, current cost analysis techniques always address (concurrent) languages featuring only addition of resources. Our technique targets a simple concurrent language with explicit operations of creation and release of resources.

The VML language specification

We target a simple concurrent and object oriented language with explicit acquire and release operations that target Virtual Machines' object abstractions. Yet small our language aims to gather the relevant operations involved in the analysis of this type of resources while dropping usual object oriented languages that do not add complexity to the theory behind this technique.

VML syntax

program :: method* { (statement;)* }
method :: type ID ( parameter* ) { (statement;)* }
parameter :: type ID
parameter :: type ID
type :: INT | VM
extendedType :: type | FUT < type >
statement :: varDecl | assignment | if | return | release
sideEffect :: exp | asyncInvoc | sync | acquire
assignment :: (extendedType)? ID = sideEffect
varDecl :: extendedType ID
return :: return exp
release :: release ID
asyncInvoc :: exp!ID( (exp (, exp)* )?)
sync :: exp.get
acquire :: new VM()
if :: if(exp) { (statement;)* } ELSE { (statement;)* }
exp :: this | se | nse
nse :: integer constants | ID | nse <= nse | nse || nse | nse && nse | nse * nse | nse + nse | nse / nse | nse - nse
se :: ve | ve <= ve | se || se | se && se
ve :: integer constants | ID | ve + se | integer values * se

Description

A vml program is a sequence of method definitions plus a main body. In vml we distinguish between types which are either integers Int or virtual machines Vm, and extended types, which also include future types. These future types let asynchronous method invocations (asyncInvoc) be typed.

A statement may be either one of the standard operations of an imperative language plus the release operation which marks the virtual machine in argument for disposal.

An sideEffect may change the state of the system. In particular, it may be an asyncInvoc that does not suspend caller�s execution: when the value computed by the invocation is needed then the caller performs a non blocking sync operation: if the value needed by a process is not available then an awaiting process is scheduled and executed. Side effect expressions also include the acquire operation that creates a new virtual machine. The intended meaning of operations taking place on different virtual machines is that they may execute in parallel, while operations in the same virtual machine interleave their evaluation (even if in the following operational semantics the parallelism is not explicit).

The execution of method invocations and creations and releases of machines always returns an erroneous value when executed on a released machine. A (pure) expression exp are the reserved identifier this, the virtual machines identifiers and the integer expressions. Since our analysis will be parametric with respect to the inputs, we parse integer expressions in a careful way. In particular we split them into size expressions se, which are expressions in Presburger arithmetics (this is a decidable fragment of Peano arithmetics that only contains addition), and non-size expressions nse, which are the other type of expressions.