Skip to content
Snippets Groups Projects
Commit dbbd3cac authored by pln's avatar pln
Browse files

Lab assignment

parent 63e74303
No related branches found
No related tags found
No related merge requests found
......@@ -42,9 +42,8 @@
#define r1_Ceiling 2
#define r2_Ceiling 3
// Analysis variables
static volatile int state;
static int job;
// some state that the execution depends on
static int state;
void work(int i)
{
......@@ -59,22 +58,15 @@ TASK(j1)
{
TRACE("j1_enter\n");
LOCK(r2);
JOB_REQUEST(j2); // job execution request for j2
if (state > 0)
{
if (state > 0) {
work(10);
}
else
{
} else {
work(5);
}
LOCK(r1);
TRACE("j1_r1_locked, before job request j2\n");
JOB_REQUEST(j2);
TRACE("j1_r1_locked, after job request j2\n");
TRACE("j1_r1_locked\n");
work(1);
TRACE("j1_r1_locked\n");
UNLOCK(r1);
UNLOCK(r2);
}
......@@ -86,15 +78,12 @@ TASK(j2)
TRACE("j2_r1_locked\n");
work(5);
UNLOCK(r1);
if (state == 100)
{
if (state == 100) {
work(2);
}
else
{
} else {
work(1);
}
TRACE("j2_exit\n");
}
......@@ -103,15 +92,21 @@ TASK(j3)
TRACE("j3_enter\n");
LOCK(r2);
TRACE("j3_r2_locked\n");
work(1);
UNLOCK(r2);
JOB_REQUEST(j1);
TRACE("j3_exit\n");
// int b = 2 * state;
// if (b < 10)
// work(10);
//
// for (int i = 0; i < state; i++)
// work(1);
}
#ifdef KLEE
/* The case when KLEE makes the path analysis */
static int job;
int main()
{
......@@ -119,23 +114,23 @@ int main()
klee_assume(job > 0 && job < 4);
klee_make_symbolic(&state, sizeof(state), "state");
klee_assume((-10 < state) && (state < 10));
switch (job)
{
default:
klee_make_symbolic(&state, sizeof(state), "state");
// check task 1
case 1:
klee_make_symbolic(&state, sizeof(state), "state");
// check task 1
EXTI1_IRQHandler();
break;
case 2:
// check task 2
klee_make_symbolic(&state, sizeof(state), "state");
EXTI2_IRQHandler();
break;
case 3:
// check task 3
klee_make_symbolic(&state, sizeof(state), "state");
EXTI3_IRQHandler();
break;
}
......@@ -146,7 +141,6 @@ int main()
static int job;
int main()
{
dwt_enable();
DWT->CYCCNT = 0;
......@@ -196,5 +190,239 @@ int main()
#endif
/*
Assignments
Assignment A)
1 connect the MCU,
2 start openocd in a new terminal shell (linux terminal e.g.
openocd -f st_nucleo_f4_itm.cfg
3 run the benchmark
> make bench
your output should look something like this
....
Opened already created database
Testcase: klee-last/test000001.ktest
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 3
object 1: name: b'state'
object 1: size: 4
object 1: data: 0
Job: j[('j3',)]
Number of instructions taken for j3: 1134
Number of instructions taken for r2: 1046
Testcase: klee-last/test000002.ktest
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 2
object 1: name: b'state'
object 1: size: 4
object 1: data: 0
Job: j[('j2',)]
Number of instructions taken for j2: 6166
Number of instructions taken for r1: 5048
Testcase: klee-last/test000003.ktest
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 2
object 1: name: b'state'
object 1: size: 4
object 1: data: 100
Job: j[('j2',)]
Number of instructions taken for j2: 7166
Number of instructions taken for r1: 5048
Testcase: klee-last/test000004.ktest
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 1
object 1: name: b'state'
object 1: size: 4
object 1: data: 0
Job: j[('j1',)]
Number of instructions taken for j1: 5186
Number of instructions taken for r2: 5104
Number of instructions taken for r1: 25
Testcase: klee-last/test000005.ktest
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 1
object 1: name: b'state'
object 1: size: 4
object 1: data: 2147483647
Job: j[('j1',)]
Number of instructions taken for j1: 10186
Number of instructions taken for r2: 10104
Number of instructions taken for r1: 25
Show to the teacher, and explain the measurements,
you should be able to relate to the code and the (nested)
"named" critical sections:
LOCK( Rx )
...
UNLOCK( Rx )
---------------------------------------------------------
Assignment B)
Perform response time analysis by hand based on the measurements
Here are the formulas (simplified)
Interference
ti= sum{⌈d(t)/ia(t’)⌉*e(t’) | t’∈ p(t’)>=p(t)}
Blocking
tb = max {cs(t’,t) | t’∈p(t’)<=p(t)}
where cs(t',t) is the max time t' holds a resource r where
⌈r⌉ >= p(t), i.e., has a ceiling larger or equal to the task we are
interested in.
Response time
tr = te + tb + ti
Fill out the table below
Job Inter arr. Deadl. WCET Block Interf. Response Time
j3 20000 20000 0
j2 30000 30000
j1 40000 40000 0 .
Why do we have 0 interference on j3 and 0 blocking for j1
Show and explain to the teacher(s)
---------------------------------------------------------
Assignment C)
Now restrict state by giving partial information (range in this case)
klee_assume((-10 < state) && (state < 10));
Rerun make bench
What significantly did change, relate to the code?
Fill in the table below, based on your new measurements.
Job Inter arr. Deadl. WCET Block Interf. Response Time
j3 20000 20000 0
j2 30000 30000
j1 40000 40000 0 .
Show and explain to the teacher(s)
---------------------------------------------------------
Assignment D)
Now enable the code in j3
int b = 2 * state;
if (b > 10)
work(1);
Identify the test cases generated for exploring both paths.
> make clean && make && make klee
> ktest-tool --write-int klee-last/*.ktest
You should get something like
ktest file : 'klee-last/test000001.ktest'
args : ['klee.bc']
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 3
object 1: name: b'state'
object 1: size: 4
object 1: data: 0
ktest file : 'klee-last/test000002.ktest'
args : ['klee.bc']
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 3
object 1: name: b'state'
object 1: size: 4
object 1: data: 6
ktest file : 'klee-last/test000003.ktest'
args : ['klee.bc']
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 2
object 1: name: b'state'
object 1: size: 4
object 1: data: 0
ktest file : 'klee-last/test000004.ktest'
args : ['klee.bc']
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 1
object 1: name: b'state'
object 1: size: 4
object 1: data: 0
ktest file : 'klee-last/test000005.ktest'
args : ['klee.bc']
num objects: 2
object 0: name: b'job'
object 0: size: 4
object 0: data: 1
object 1: name: b'state'
object 1: size: 4
object 1: data: 1
Show and explain to the teacher(s)
--------------------------------------------
Assignment D)
Figure out how to isolate the analysis to j3.
Show and explain to the teacher(s)
--------------------------------------------
Assignment E)
Enable the code in k3.
int b = 2 * state;
if (b < 10)
work(10);
for (int i = 0; i < state; i++)
work(1);
Now re-run the make bench.
Identify the WCET for j3.
What is the reason a specific state gives the WCET.
Show and explain to the teacher(s)
Play around, have fun with the tool!!!!!
*/
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment