From dbbd3cac94002ef88503e6254a57ce01f6595130 Mon Sep 17 00:00:00 2001
From: pln <Per Lindgren>
Date: Mon, 6 Mar 2017 13:29:26 +0000
Subject: [PATCH] Lab assignment
---
src/main.c | 310 ++++++++++++++++++++++++++++++++++++++++++++++-------
1 file changed, 269 insertions(+), 41 deletions(-)
diff --git a/src/main.c b/src/main.c
index 3621eae..c3f6cff 100644
--- a/src/main.c
+++ b/src/main.c
@@ -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,23 +58,16 @@ TASK(j1)
{
TRACE("j1_enter\n");
LOCK(r2);
- JOB_REQUEST(j2); // job execution request for j2
-
- if (state > 0)
- {
- work(10);
- }
- 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");
- UNLOCK(r1);
+ if (state > 0) {
+ work(10);
+ } else {
+ work(5);
+ }
+ LOCK(r1);
+ TRACE("j1_r1_locked\n");
+ work(1);
+ TRACE("j1_r1_locked\n");
+ UNLOCK(r1);
UNLOCK(r2);
}
@@ -83,18 +75,15 @@ TASK(j2)
{
TRACE("j2_enter\n");
LOCK(r1);
- TRACE("j2_r1_locked\n");
- work(5);
+ TRACE("j2_r1_locked\n");
+ work(5);
UNLOCK(r1);
- if (state == 100)
- {
- work(2);
- }
- else
- {
- work(1);
- }
+ if (state == 100) {
+ work(2);
+ } else {
+ work(1);
+ }
TRACE("j2_exit\n");
}
@@ -102,16 +91,22 @@ TASK(j3)
{
TRACE("j3_enter\n");
LOCK(r2);
- TRACE("j3_r2_locked\n");
-
- work(1);
+ 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!!!!!
+
*/
--
GitLab