HW-example
- Two software components, c1 and c2, where c1 has 3 implementations (1a, 1b and 1c) and c2 has only one (2a)
- Two hardware components, res1 and res2 with load provisions of 0.4 for res1 and 0.7 for res2
- Implementations 1a and 1c do require c2, whereas 1b does not require c2
- All implementations have requirements for the load property
load-requirements
- component c1
- 1a: max 0.5
- 1b: max 0.8
- 1c: max 0
- component c2
- 2a: max 0.5
load-provision
- res1 = 0.4
- res2 = 0.7
resulting constraints
- load-c1-res1: 0.4 <= 0.5 1a-res1 + 0.8 1b-res1 + 0 1c-res1
- load-c2-res1: 0.4 <= 0.5 2a-res1
- load-c1-res2: 0.7 <= 0.5 1a-res2 + 0.8 1b-res2 + 0 1c-res2
- load-c2-res2: 0.7 <= 0.5 2a-res2
Problem: if c2 not chosen (e.g. because not needed for impl-11), constraint load-c2-res1 is always violated
- Constraint would look like
0.4 <= 0.5 * 0
, i.e.0.4 <= 0
resulting constraints with max-fix
- Need to know or compute a maximum value for property load. The value need to be greater than the left hand side value and not creating zero coefficients.
- Replace coefficients with "$maximum - $oldValue"
- Use ">=" as constraint sense
Now if c2 is not chosen, the load-c2-res1 is correctly fulfilled: 0.6 >= 0.5 * 0
, i.e. 0.6 >= 0
- load-c1-res1: 0.6 >= 0.5 1a-res1 + 0.2 1b-res1 + 1 1c-res1
- load-c2-res1: 0.6 >= 0.5 2a-res1
- load-c1-res2: 0.3 >= 0.5 1a-res2 + 0.2 1b-res2 + 1 1c-res2
- load-c2-res2: 0.3 >= 0.5 2a-res2
resulting constraints with max-fix and scheme-insights
hardware-properties → prop.ishw = #t
create "right-hand-side–templates" for each resource-type (e.g. Cubieboard), property and comp
if comp=max, apply 'maximum inversion'
example: 0.5 1a-RES + 0.8 1b-RES + 0 1c-RES
creating template_type,comp,property
for-each Resource pe, Property prop, Comp c and Comparator comparator
constraints += (eval prop-on-pe) (comp->string comparator) (deploy template_(type-of pe),c,prop pe)
- (eval prop pe) evalutates the property on the resource
- (comp->string comparator) gets a string representation of the comparator
- (deploy template pe) instantiates the template on the resource
- only add constraint, if template exists, template is not empty and property exists on pe
software-properties
for-all comp c
for-all (req-comp-map c) (reqC,impls) ; impls, that require the component reqC
for-all (impls-of reqC) rci
constraint += "+" (eval prop rci)
constraint += ">="|"="
for-all impls i → for-all (mode-of i) m → for-all (clause-in m) cl → for-all pe
constraint += "+" (eval prop cl) (varname m-deployed-on-pe)
SW-Example
response-time-of-c2-requirements
- 1a: max size == max 50
- 1b: -
- 1c: max -1 never true
response-time-of-c2-provisions
- 2a = 0.5
- 2b = 0.6
resulting constraints
- rtC2-impl1: 0.5 b#2a + 0.6 b#2b <= 50 b#1a + -1 b#1c
or
- rtC2a-impl1: 0.5 b#2a <= 50 b#1a + -1 b#1c
- rtC2b-impl1: 0.6 b#2b <= 50 b#1a + -1 b#1c
?
Use maximum inversion with max = 2
- rtC2-impl1: 1.5 b#2a + 1.4 b#2b >= -48 b#1a + 3 b#1c
or
- rtC2a-impl1: 1.5 b#2a >= -48 b#1a + 3 b#1c
- rtC2b-impl1: 1.4 b#2b >= -48 b#1a + 3 b#1c
?
SW-Example 2
Assuming 2a only impl of comp 2.
20 2a <= 50 1a + 10 1c
- 1a OK, 1c correctly bad, 1b wrongly bad
set max 30:
10 2a >= -20 1a + 20 1c
- 2a=1 → 1a,1b,1c correct. 2a=0 → 1a wrongly bad, 1b,1c correct.
set max 60:
40 2a >= 10 1a + 50 1c
- 2a=1 → 1a,1b,1c correct. 2a=0 → 1a,1b,1c correct.
set max 11:
9 2a >= -39 1a + 1 1c
- 1a,1c correct. 1b still wrongly bad
Some formal correctness considerations
X 2a <= Y 1a + Z 1c with Z < X < Y
set max M with M > max(X,Y,Z)
X' = M - X
Y' = M - Y
Z' = M - Z
X' 2a >= Y' 1a + Z' 1c if X' != 0 and Y' != 0 and Z' != 0
and
X' 2a >= 0 (for the selection of an impl not needing comp 2)
and
0 <= Y (to ensure the selection of 2a)
0 <= Z –||–
It should be true, that X' > Y'
and Z' > X'
.
M - X > M - Y | -M
- X > - Y | *(-1) if X != 0 and Y != 0
X < Y
M - Z > M - X | -M
- Z > - X | *(-1) if X != 0 and Z != 0
Z < X
with multiple providing impls
X1 2a + X2 2b <= Y 1a + Z 1c with Z < X1 < Y // not sure about reqs for X2
set max M with M > max(X1,X2,Y,Z)
X1' = M - X1
X2' = M - X2
Y' = M - Y
Z' = M - Z
X1' 2a + X2' 2b >= Y' 1a + Z' 1c trivially: if {X1',X2',Y',Z'} != 0 ← guaranteed by Def. of M
and
X1' 2a + X2' 2b >= 0 (for the selection of an impl not needing comp 2)
and
0 <= Y (to ensure the selection of 2a)
0 <= Z –||–
assuming 2a and 2b the only impls of comp 2.
right or wrong? use 1a ^ 1c → 2a ^ 2b. 1b → #t = 2a | 2b (^ is xor, | is or)
- 2a=1: 1a correctly good, 1c correctly bad, 1b wrongly bad
- 2b=1: 1a correctly bad, 1c correctly bad, 1b wrongly bad
- 2*=0: 1a wrongly good, 1c wrongly good, 1b correctly good
20 2a + 60 2b <= 50 1a + 10 1c
set max 30
10 2a + -30 2b >= -20 1a + 20 1c
- 2a=1,2b=0 → 1a,1b,1c correct.
- 2a=0,2b=1 → 1a,1c correct, 1b wrongly bad.
- 2*=0 → 1a wrongly good, 1b,1c correct.
set max 70
50 2a + 10 2b >= 20 1a + 60 1c
- 2a=1,2b=0 → 1a,1b,1c correct.
- 2a=0,2b=1 → 1a,1b,1c correct.
- 2*=0 → 1a,1b,1c correct.
Another issue
- Q: Are there actually properties for which it make sense to have both min AND max constraints?
- A: for now, assume there are none.
The request
constraint
- response-time-C1 <= 0.3
provisions
- 1a = 0.2
- 1b = 0.4
- 1c = 0.2
expected outcome
- only 1a or 1c can be chosen
- because of architectural constraint, either 1a or 1c can be chosen
- because of request target constraint, either 1a or 1c have to be chosen
the initial constraint
0.2 1a##cb1 + 0.2 1a##cb2 + 0.4 1b##cb1 + 0.4 1b##cb2 + 0.2 1c##cb1 + 0.2 1c##cb2 <= 0.3
the constraint with max-fix
- maximum+1 = 1.4
1.2 1a##cb1 + 1.2 1a##cb2 + 1.0 1b##cb1 + 1.0 1b##cb2 + 1.2 1c##cb1 + 1.2 1c##cb2 >= 1.1