main.c

//#define KLEE
#define JOB 1

#ifdef KLEE
#include "SRP_klee.h"
#elif KLEE_WCET
#include "SRP_wcet.h"
#else
#include "main.h"
#define enable_itm
#endif


// job bindings
#define j1_IRQn EXTI1_IRQn
#define j2_IRQn EXTI2_IRQn
#define j3_IRQn EXTI3_IRQn

#define j1_IRQh EXTI1_IRQHandler
#define j2_IRQh EXTI2_IRQHandler
#define j3_IRQh EXTI3_IRQHandler

// job priorities
#define j1_Prio 1
#define j2_Prio 2
#define j3_Prio 3

// resource ceilings
#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++;
    }
}

TASK(j1)
{
    LOCK(r2);

    JOB_REQUEST(j2); 			// job execution request for j2

    if (state > 0)
    {
        work(10);
    }
    else
    {
        work(5);
    }

    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);
}

TASK(j2)
{
#ifdef enable_itm
    trace_printf("j2_enter\n");
#endif
    LOCK(r1);
#ifdef enable_itm
    trace_printf("j2_r1_locked\n");
#endif
    UNLOCK(r1);
#ifdef enable_itm
    trace_printf("j2_exit\n");
#endif
}

int main()
{
#ifdef enable_itm
    trace_printf("\nInit\n");
#endif

#ifndef KLEE

    dwt_enable();
    DWT->CYCCNT = 0;
#ifndef KLEE_WCET

    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;

    /* 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");
    //IRQh(j1);
    EXTI1_IRQHandler();

#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
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)
*/