57 lines
1.6 KiB
C
57 lines
1.6 KiB
C
#ifndef TASK01_MUTEX_H
|
|
#define TASK01_MUTEX_H
|
|
|
|
#include <stdint.h>
|
|
|
|
#include "FreeRTOS.h"
|
|
#include "semphr.h"
|
|
#include "task.h"
|
|
#include "task01_mutex_model.h"
|
|
|
|
#define FC08_TASK_STACK_WORDS 256U
|
|
#define FC08_LOW_PRIORITY 1U
|
|
#define FC08_MEDIUM_PRIORITY 2U
|
|
#define FC08_HIGH_PRIORITY 3U
|
|
#define FC08_VERIFIER_PRIORITY 0U
|
|
#define FC08_EVENT_CAPACITY 12U
|
|
#define FC08_TIMEOUT_TICKS 20U
|
|
|
|
typedef struct MutexExperiment
|
|
{
|
|
SemaphoreHandle_t mutex;
|
|
TaskHandle_t low_handle;
|
|
TaskHandle_t medium_handle;
|
|
TaskHandle_t high_handle;
|
|
TaskHandle_t verifier_handle;
|
|
UBaseType_t inherited_priority;
|
|
UBaseType_t restored_priority;
|
|
TaskHandle_t holder_while_contended;
|
|
eTaskState medium_state_while_inherited;
|
|
uintptr_t low_sp;
|
|
uintptr_t high_sp;
|
|
uintptr_t medium_sp;
|
|
uint32_t protected_value;
|
|
uint32_t medium_started;
|
|
uint32_t medium_started_while_inherited;
|
|
uint32_t high_acquired;
|
|
uint32_t low_done;
|
|
uint32_t high_done;
|
|
uint32_t medium_done;
|
|
uint32_t pass;
|
|
uint32_t evidence_digest;
|
|
} MutexExperiment;
|
|
|
|
extern MutexExperiment g_fc08;
|
|
extern MutexEvidence g_fc08_events[ FC08_EVENT_CAPACITY ];
|
|
extern volatile uint32_t g_fc08_event_count;
|
|
extern volatile uint32_t g_fc08_last_checkpoint;
|
|
extern volatile uint32_t g_fc08_pass;
|
|
|
|
void fc08_checkpoint_committed( uint32_t point, const void * subject );
|
|
void fc08_low_entry( void * context );
|
|
void fc08_medium_entry( void * context );
|
|
void fc08_high_entry( void * context );
|
|
void fc08_verifier_entry( void * context );
|
|
|
|
#endif
|