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 |
k |
e |
f |
i |
j |
|
z1 |
0 |
0 |
0 |
0 |
0 |
z2 |
7 |
7 |
7 |
7 |
7 |
l |
m |
n |
|
z1 |
1 |
1 |
1 |
z2 |
1 |
1 |
1 |
a |
b |
|
z1 |
0 |
10 |
z2 |
10 |
0 |
a |
b |
e |
f |
i |
j |
|
z1 |
10 |
10 |
10 |
10 |
10 |
10 |
z2 |
0 |
0 |
0 |
0 |
0 |
0 |
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.
We carried out the following three experiments, comparing
compositional and incremental re-resolution approaches over five
availability zones
Adding two new sub-components.
Transcript of this experiment obtained from the incremental SMT
re-resolution tool: comp-inc-change1.txt
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