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

prepare for lab (wcet)

parent 03cb7333
No related branches found
No related tags found
No related merge requests found
//#define KLEE //#define KLEE
#define JOB 1
#ifdef KLEE #ifdef KLEE
#include "SRP_klee.h" #include "SRP_klee.h"
...@@ -75,6 +74,8 @@ TASK(j2) ...@@ -75,6 +74,8 @@ TASK(j2)
LOCK(r1); LOCK(r1);
#ifdef enable_itm #ifdef enable_itm
trace_printf("j2_r1_locked\n"); trace_printf("j2_r1_locked\n");
work(5);
#endif #endif
UNLOCK(r1); UNLOCK(r1);
#ifdef enable_itm #ifdef enable_itm
...@@ -82,6 +83,28 @@ TASK(j2) ...@@ -82,6 +83,28 @@ TASK(j2)
#endif #endif
} }
TASK(j3) {
#ifdef enable_itm
trace_printf("j3_enter\n");
#endif
LOCK(r1);
#ifdef enable_itm
trace_printf("j3_r1_locked\n");
#endif
work(1);
UNLOCK(r1);
JOB_REQUEST(j1);
#ifdef enable_itm
trace_printf("j3_exit\n");
#endif
}
#ifdef KLEE_WCET
// will be set by gdb
static volatile int wcet_task;
#endif
int main() int main()
{ {
#ifdef enable_itm #ifdef enable_itm
...@@ -94,6 +117,7 @@ int main() ...@@ -94,6 +117,7 @@ int main()
DWT->CYCCNT = 0; DWT->CYCCNT = 0;
#ifndef KLEE_WCET #ifndef KLEE_WCET
// this will be run in the production code
SETPRIO(j1); // Set HW priorities SETPRIO(j1); // Set HW priorities
SETPRIO(j2); SETPRIO(j2);
SETPRIO(j3); SETPRIO(j3);
...@@ -101,8 +125,8 @@ int main() ...@@ -101,8 +125,8 @@ int main()
ENABLE(j2); ENABLE(j2);
ENABLE(j3); ENABLE(j3);
JOB_REQUEST(j1); // comment out in assignment c //JOB_REQUEST(j1); // comment out in assignment c
//JOB_REQUEST(j3); // use in assignment c JOB_REQUEST(j3); // use in assignment c
BREAKPOINT; BREAKPOINT;
while (1) ; while (1) ;
...@@ -122,92 +146,19 @@ int main() ...@@ -122,92 +146,19 @@ int main()
#elif (JOB == 1) #elif (JOB == 1)
// check task 1 // check task 1
klee_make_symbolic(&state, sizeof(state), "state"); klee_make_symbolic(&state, sizeof(state), "state");
//IRQh(j1);
EXTI1_IRQHandler(); EXTI1_IRQHandler();
#elif (JOB == 2)
// check task 2
klee_make_symbolic(&state, sizeof(state), "state");
EXTI2_IRQHandler();
#elif (JOB == 3)
// check task 3
klee_make_symbolic(&state, sizeof(state), "state");
EXTI3_IRQHandler();
#endif #endif
} }
/* enable in assignment c
TASK(j3) {
#ifdef enable_itm
trace_printf("j3_enter\n");
#endif
LOCK(r2);
#ifdef enable_itm
trace_printf("j3_r2_locked\n");
#endif
UNLOCK(r2);
JOB_REQUEST(j1);
#ifdef enable_itm
trace_printf("j3_exit\n");
#endif
}
//
*/
/* /*
Assignments Assignments
a) Run the program, you should get
0 Init
1 j1_enter
2 j2_enter
3 j2_r1_locked
4 j2_exit
5 j1 after job request j2
6 j1_r1_locked, before job request j2
7 j1_r1_locked, after job request j2
8 j2_enter
9 j2_r1_locked
10 j2_exit
11 j1_exit
b)
Fill in the table
Current prio , System Ceiling, Stack , Pending Tasks
0 0 , 0 , idle, , {j1}
1 1 , 0 , idle:j1 , {j2}
2 2 , 1 , idle:j1:j2, {}
3 2 , 2 , idle:j1:j2, {}
4 2 , 1 , idle:j1:j2, {}
5 1 , 1 , idle:j1 , {}
6 ? , ? , ? , {?}
7 ? , ? , ? , {?}
8 ? , ? , ? , {?}
9 ? , ? , ? , {?}
10 ? , ? , ? , {?}
11 ? , ? , ? , {?}
Notice the values are immediately after execution of the
corresponding print.
Show to teacher(s)
c)
add a third task at priority 3
TASK(j3) {
#ifdef enable_itm
trace_printf("j3_enter\n");
#endif
LOCK(r2);
#ifdef enable_itm
trace_printf("j3_r2_locked\n");
#endif
UNLOCK(r2);
JOB_REQUEST(j1);
#ifdef enable_itm
trace_printf("j3_exit\n");
#endif
}
Compute and set the new ceiling value(s)
Change line 38, so that
make a new table as above for the complete trace
Show to teacher(s)
*/ */
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment