From a432fe129cca992af63fb33059d63d86a8fb1eff Mon Sep 17 00:00:00 2001
From: pln <Per Lindgren>
Date: Sun, 5 Mar 2017 20:43:56 +0000
Subject: [PATCH] main restrucuring symbolic jobs, SRP.x files simplified
---
include/SRP.h | 2 +-
include/SRP_wcet.h | 14 +--
src/main.c | 242 +++++++++++++++++++++++----------------------
3 files changed, 128 insertions(+), 130 deletions(-)
diff --git a/include/SRP.h b/include/SRP.h
index 09741d4..b182d99 100644
--- a/include/SRP.h
+++ b/include/SRP.h
@@ -34,5 +34,5 @@
#define TASK(J) void IRQh(J) ()
-#define BREAKPOINT { asm volatile("" ::: "memory"); }
+#define BREAKPOINT { asm volatile("nop" ::: "memory"); }
diff --git a/include/SRP_wcet.h b/include/SRP_wcet.h
index 787cea2..609d5ef 100644
--- a/include/SRP_wcet.h
+++ b/include/SRP_wcet.h
@@ -45,7 +45,6 @@ typedef struct locks
} locks;
-
int event_count = 0;
/* Create array containing structs of type locks */
@@ -55,26 +54,17 @@ locks eventlist[MAX_NUM_LOCKS];
#define TRACE_EVENT(event, el)({eventlist[event_count].time = DWT->CYCCNT; eventlist[event_count].action = event; eventlist[event_count].elem = el; event_count+=1;})
-// #define Ceiling(R) (R##_Ceiling)
-// #define Code(J) (J##_Code)
-// #define IRQn(J) (J##_IRQn)
-// #define H(X) ((1 << __NVIC_PRIO_BITS)-X)
#define IRQh(J) (J##_IRQh)
-// #define BARRIER_LOCK { }
-// #define BARRIER_UNLOCK { }
#define JOB_REQUEST(J) { }
#define LOCK(X) TRACE_EVENT(L, X);
#define UNLOCK(X) TRACE_EVENT(R, X);
-// #define SETPRIO(J) { }
-// #define ENABLE(J) { }
-
#define TASK(J) void IRQh(J) ()
-#define BREAKPOINT { asm volatile("" ::: "memory"); }
+#define BREAKPOINT
void finish_execution(void) {}
-void terminate_execution(void) {}
+//void terminate_execution(void) {}
diff --git a/src/main.c b/src/main.c
index ff3b78e..5769321 100644
--- a/src/main.c
+++ b/src/main.c
@@ -1,14 +1,28 @@
//#define KLEE
+#define KLEE_WCET
#ifdef KLEE
#include "SRP_klee.h"
-#elif KLEE_WCET
+#define TRACE(X) {}
+
+#elif defined KLEE_WCET
#include "SRP_wcet.h"
+#define TRACE(X) {}
+
#else
-#include "main.h"
-#define enable_itm
-#endif
+// Production code
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+#include "dwt.h"
+#include "Trace.h"
+
+#include <stm32f401xe.h>
+#include "SRP.h"
+#define TRACE(X) trace_printf(X)
+#endif
// job bindings
#define j1_IRQn EXTI1_IRQn
@@ -28,137 +42,131 @@
#define r1_Ceiling 2
#define r2_Ceiling 1
-static int state;
-
-void work(int i)
-{
- volatile int k =0;
- for (int j =0; j < 100 * i; j++)
- {
- k++;
- }
+void work(int i) {
+ volatile int k = 0;
+ for (int j = 0; j < 100 * i; j++) {
+ k++;
+ }
}
-TASK(j1)
-{
- LOCK(r2);
+TASK(j1) {
+ TRACE("j1_enter\n");
+ LOCK(r2);
+ JOB_REQUEST(j2); // job execution request for j2
- JOB_REQUEST(j2); // job execution request for j2
+ if (state > 0) {
+ work(10);
+ } else {
+ work(5);
+ }
- if (state > 0)
- {
- work(10);
- }
- else
- {
- work(5);
- }
+ LOCK(r1);
+ TRACE("j1_r1_locked, before job request j2\n");
- LOCK(r1);
-#ifdef enable_itm
- trace_printf("j1_r1_locked, before job request j2\n");
-#endif
- JOB_REQUEST(j2);
-#ifdef enable_itm
- trace_printf("j1_r1_locked, after job request j2\n");
-#endif
- UNLOCK(r1);
- UNLOCK(r2);
+ JOB_REQUEST(j2);
+ TRACE("j1_r1_locked, after job request j2\n");
+ UNLOCK(r1);
+ UNLOCK(r2);
}
-TASK(j2)
-{
-#ifdef enable_itm
- trace_printf("j2_enter\n");
-#endif
- LOCK(r1);
-#ifdef enable_itm
- trace_printf("j2_r1_locked\n");
- work(5);
-
-#endif
- UNLOCK(r1);
-#ifdef enable_itm
- trace_printf("j2_exit\n");
-#endif
+TASK(j2) {
+ TRACE("j2_enter\n");
+ LOCK(r1);
+ TRACE("j2_r1_locked\n");
+ work(5);
+ UNLOCK(r1);
+ TRACE("j2_exit\n");
}
TASK(j3) {
-#ifdef enable_itm
- trace_printf("j3_enter\n");
-#endif
+ TRACE("j3_enter\n");
LOCK(r1);
-#ifdef enable_itm
- trace_printf("j3_r1_locked\n");
-#endif
+ TRACE("j3_r1_locked\n");
work(1);
-
UNLOCK(r1);
JOB_REQUEST(j1);
-#ifdef enable_itm
- trace_printf("j3_exit\n");
-#endif
+ TRACE("j3_exit\n");
}
-#ifdef KLEE_WCET
-// will be set by gdb
-static volatile int wcet_task;
-#endif
-
-int main()
-{
-#ifdef enable_itm
- trace_printf("\nInit\n");
-#endif
-
-#ifndef KLEE
-
- dwt_enable();
- DWT->CYCCNT = 0;
-#ifndef KLEE_WCET
-
- // this will be run in the production code
- SETPRIO(j1); // Set HW priorities
- SETPRIO(j2);
- SETPRIO(j3);
- ENABLE(j1); // Enable HW sources
- ENABLE(j2);
- ENABLE(j3);
-
- //JOB_REQUEST(j1); // comment out in assignment c
- JOB_REQUEST(j3); // use in assignment c
-
- BREAKPOINT;
- while (1) ;
- return 0;
+#ifdef KLEE
+/* The case when KLEE makes the path analysis */
+static int state;
+static int job;
+
+int main() {
+ klee_make_symbolic(&job, sizeof(job), "job");
+
+ switch (job) {
+ case 1:
+ // check task 1
+ klee_make_symbolic(&state, sizeof(state), "state");
+ 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;
+ }
+
+#elif defined KLEE_WCET
+/* The case when gdb runs WCET benchmarking */
+static int state;
+static int job;
+int main() {
+
+ dwt_enable();
+ DWT->CYCCNT = 0;
+
+ switch (job) {
+ case 1:
+ TRACE_EVENT(S, j1);
+ EXTI1_IRQHandler();
+ TRACE_EVENT(E, j1);
+ break;
+ case 2:
+ TRACE_EVENT(S, j2);
+ EXTI2_IRQHandler();
+ TRACE_EVENT(E, j2);
+ break;
+ case 3:
+ TRACE_EVENT(S, j3);
+ EXTI3_IRQHandler();
+ TRACE_EVENT(E, j3);
+ break;
+ }
+
+ finish_execution(); // gdb breakpoint
+ // terminate_execution();
+}
- /* The case when NOT running WCET benchmark nor KLEE-analysis */
#else
-
- TRACE_EVENT(S, j1);
- EXTI1_IRQHandler();
- TRACE_EVENT(E, j1);
-#endif
-
- finish_execution();
- terminate_execution();
-
-#elif (JOB == 1)
- // check task 1
- klee_make_symbolic(&state, sizeof(state), "state");
- 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
+// this will be run in the production code
+int main() {
+ TRACE("\nInit\n");
+ SETPRIO(j1); // Set HW priorities
+ SETPRIO(j2);
+ SETPRIO(j3);
+ ENABLE(j1);// Enable HW sources
+ ENABLE(j2);
+ ENABLE(j3);
+
+ JOB_REQUEST(j3);// use in assignment c
+
+ BREAKPOINT
+ ;
+
+ while (1)
+ ;
+ return 0;
}
+#endif
/*
-Assignments
-*/
+ Assignments
+ */
--
GitLab