Efficient Re-resolution of SMT Specifications for Evolving Software Architectures


Abstract

We present a generic method for the efficient constraint re-resolution of a component-based software architecture after
changes such as addition, removal and modification of components.
Given a formal description of an evolving system as a constraint-specification problem, our method identifies and
executes the re-resolution steps required to verify the system's compliance  with constraints after each change.
At each step,  satisfiability-modulo theory (SMT) techniques determine the satisfiability of component constraints expressed as
logical formulae over suitably chosen theories of arithmetic, reusing results obtained in previous steps.
We illustrate the application of the approach on a constraint-satisfaction problem arising from cloud-deployed software services.
The incremental method is shown to re-resolve system constraints in a fraction of the time taken by standard SMT resolution.

Download the incremental SMT source code here: incremental-tool.zip. Installation instructions: readme.txt

Case Study

Architecture

Consider the following case study of a service S with the following components:
  1. one website component web,
  2. two application components app1 and app2,
  3. two database components db1 and db2.
Each component has two sub-components labelled alphabetically A to J. In total, S is a service with 16 components.

We express the system's architecture by the component term

S = c(web,c(db1,c(db2,c(app1,app2)))), where web = c(A,B), db1 = c(C,D), db2= c(E,F), app1 = c(G,H), app2 = c(I,J)

Requirements

The service S is distributed over p cloud availability zones numbered 1 to p, according to the following requirements:
  1. all sub-components A- J have between 1 and 20 instances deployed across p availability zones
  2. A has exactly 10 instances
  3. B cannot be deployed on zone 2
  4. sub-components of app1 must be distributed across at least 2 zones
  5. db1 sub-components cannot be deployed on zone 1
  6. app2 and db2 must be distributed identically across zones

Compositional Resolution

Suppose we wish to deploy the case study system S across p = 2 availability zones according to Requirements (1) - (7)
Each component c in the case study system S is modelled as a set Mc = {cz1,...czp} of integer typed variables, such that
"czi = n" models the scenario in which "n" virtual instances of the component c is deployed on the ith availability zone, 1 <= i <= p.

The case study system is resolved by compositional SMT resolution in seven steps, where each step represents the resolution of each component's requirements.
  1. s+ app2 + db2 + e + f + i + j 
  2. a
  3. b
  4. c
  5. d
  6. g
  7. h
yielding the solution mapping v : {z1,z2} -> Integer in 0.058 seconds


a
b
c
d
e
f
g
h
i
j
z1
10
1
0
1
0
0
1
1
0
0
z2
0
0
1
0
1
1
0
0
1
1


Change Scenarios

We outline some change scenarios handled by the incremental SMT implementation.

1. sub-component addition to app2

Suppose that a new sub-component K is added to the component app2 such that there must be at least 7 instances of K deployed and Requirement (6) must remain satisfied.

The architecture of the service is updated by the substitution:

S' = S[app2/c(k,c(I,J))]

The incremental re-resolution obtained a new satisfiable solution v' obtained from the previous resolution solution v in 0.004 seconds:


k
e
f
i
j
z1
0
0
0
0
0
z2
7
7
7
7
7

obtaining v1.

2. component addition of db3

Suppose that the system has a new database component to be deployed, comprising 3 sub-components L,M,N such that each sub-component must be deployed over all zones (2).

The architecture of the service is updated by the substitution:

S'' = S'[S'/ c(db3,c(web,c(db1,c(db2,c(app1,app2)))))]

The incremental re-resolution updates the previous resolution solution v' in 0.008 seconds with the following values


l
m
n
z1
1
1
1
z2
1
1
1

obtaining v''.

3. requirement addition to web

Suppose that the web component has an added requirement that all sub-components must be in the same zone

The architecture of the service remains the same, but the web component is associated with the following logical formula (in Z3 notation):

Web requirements: (assert ( = (+ az2 az1 ) (+ bz2 bz1 ) ))

The incremental re-resolution takes 0.007 seconds and updates v'' to obtain the following values


a
b
z1
0
10
z2
10
0

and we note that this solution maintains Requirement (3) that no instance of b is deployed on Zone 2.

4. requirement addition to service

Suppose that we add a requirement to the service that the web component must be identically distributed to app2 (and by extension db2)

The architecture of the service remains the same, but the service component is associated with the following logical formulae (in Z3 notation):

(assert (and ( = ez2 fz2 ) (and ( = ez1 fz1 ) )))
(assert (and ( = ez2 kz2 ) (and ( = ez1 kz1 ) )))
(assert (and ( = ez2 az2 ) (and ( = ez1 az1 ) )))
(assert (and ( = az2 bz2 ) (and ( = az1 bz1 ) )))
(assert (and ( = ez2 iz2 ) (and ( = ez1 iz1 ) )))
(assert (and ( = iz2 jz2 ) (and ( = iz1 jz1 ) )))

e.g. all sub-components A,B, E,F I,J of web, app2 and db2 respectively have identical distributions across zones (subject to all previous requirements)

The incremental re-resolution takes 0.006 seconds and updates v''' to obtain the following values


a
b
e
f
i
j
z1
10
10
10
10
10
10
z2
0
0
0
0
0
0


The transcript from our incremental SMT resolution tool for the above changes is available: changeScenariosTranscript.txt

Domain Specific Language

We developed a domain specific language to translate high-level requirements such as those listed in (1) - (7) into logical formulae.
The following table shows the high level English requirement and it's equivalent formula expressed in Microsoft's Z3 assertion language.

Cloud Deployment Requirement in English
Formula Speciccation in Z3 Assertion Language
Each zone zi has a non-negative number of c instances deployed,j=1..p
(assert( >= c_z1 0)),..., (assert( >= c_zp 0))
No instance of function c must be deployed on zi
(assert (= c_zi 0))
c must have at least x instances on zi
(assert (>= c_zi) x)
(a) c must have at least x instances
(b) c must have at most x instances
(c) c must have exactly x instances
(a) (assert (>= (+ c_z1 (+ c_z2 (+ .... c_zp))) x))
(b) (assert (<= (+ c_z1 (+ c_z2 (+ .... c_zp))) x))
(c) (assert (=  (+ c_z1 (+ c_z2 (+ .... c_zp)))  x))
all instances of c must be in zone zi
We formalise a constraint for "all instances of c on zi"
(assert (= c_zi c_N))

For every other zone zk in z1...z_j-1,z_j+1,...,zp, there are no instances of c on zk
(assert (= c_zk 0)) ;kth has no c instances
(a) instances of c must be in the same zone
(b) instances of c must be distributed across exactly x zones
(c) instances of c must be distributed across at least x zones

Formalised for three zones, for readability.

Consider the case of c across three zones:
(declare-const c_z1 Int)
(declare-const c_z2 Int)
(declare-const c_z3 Int)
(declare-const c_N Int)
(declare-const deploySum Int)
(declare-const c_z1Deploy Int)
(declare-const c_z2Deploy Int)
(declare-const c_z3Deploy Int)

Suppose we have 7 instances of c to be deployed
(assert (= c_N 7))
(assert (= c_N (+ c_z1 (+ c_z2 c_z3)) ))

Each c_ziDeploy variable is 1 if c is deployed on zi (> c_zi  0) and 0 otherwise
(assert(= c_z1Deploy (ite (> c_z1  0) 1 0)))
(assert(= c_z2Deploy (ite (> c_z2  0) 1 0)))
(assert(= c_z3Deploy (ite (> c_z3  0) 1 0)))

Now sum them up:
(assert (= deploySum (+c_z1Deploy (+ c_z2Deploy c_z3Deploy))))

(a) We assert that c should only be deployed in the same zone:
(assert (= deploySum 1))

(b) We assert that c should be deployed across exactly x availability zones:
(assert (= deploySum x))

(c) We assert that c should be deployed across at least x availability zones:
(assert (>= x deploySum))
c and fj must have the same number of instances
(assert (= c_N fj_N))
instances of c and fj must be distributed similarly across availability zones
(assert (= c_N fj_N))

(assert (= c_z1 fj_z1)) ;identical number of instances of c and fj on zone z1
...
(assert (= c_zp fj_zp)) ;identical number of instances of c and fj on zone zp


We developed a JAVA library which contains methods that translate high-level cloud deployment concgurations into formulae written in Z3's assertion language.


Tool Performance

We performed compositional and incremental resolution on increasingly larger systems. Initially, the system comprises

We carried out the following three experiments, comparing compositional and incremental re-resolution approaches over five availability zones

Change Experiment 1

Adding two new sub-components.
Transcript of this experiment obtained from the incremental SMT re-resolution tool: comp-inc-change1.txt

Change Experiment 2

Adding two new components, each with 10 sub-components, ensuring each component's sub-components have identical distributions.
Transcript of this experiment obtained from the incremental SMT re-resolution tool: comp-inc-change2.txt

Change Experiment 3

Adding two new components, each with 10 sub-components, each constraining their sub-components to identical distributions as in the
previous experiment but with an additional service-level requirement which constrains each component to have the same number of instances.
Transcript of this experiment obtained from the incremental SMT re-resolution tool: comp-inc-change3.txt


Kenneth Johnson and Radu Calinescu Feb 25th 2014