diff --git a/generator/graph/GenerateAssertions.py b/generator/graph/GenerateAssertions.py
index 80c260bf16ad8e08d53b1666f630be2323da7fe5..513be6b9e6b2c19662ac9911f7b374c61f7552db 100644
--- a/generator/graph/GenerateAssertions.py
+++ b/generator/graph/GenerateAssertions.py
@@ -9,6 +9,8 @@ class AssertionType(Enum):
TaskWasKickoffed = 2
TaskWasNotKickoffed = 3
+ EventsCheck = 4
+
class Assertion:
def __init__(self, _type, _arguments, prio = 0):
@@ -85,6 +87,20 @@ class GenerateAssertionsPass(Analysis):
if state.was_surely_kickoffed(subtask):
ret.append(Assertion(AssertionType.TaskWasKickoffed, [subtask],
prio = prio * 1.5))
+ # For each event this task can receive, we can derive an assertions
+ events_set = []
+ events_cleared = []
+ for event in subtask.events:
+ SET = state.is_event_set(subtask, event)
+ CLEARED = state.is_event_cleared(subtask, event)
+ assert SET or CLEARED
+
+ if SET == 0 and CLEARED == 1:
+ events_cleared.append(event)
+ if SET == 1 and CLEARED == 0:
+ events_set.append(event)
+ if events_set or events_cleared:
+ ret.append(Assertion(AssertionType.EventsCheck, [subtask, events_cleared, events_set]))
return ret
def state_assertions_before(self, abb):
diff --git a/generator/graph/PreciseSystemState.py b/generator/graph/PreciseSystemState.py
index 1e55b6caddc4750654a77eae5b387646e85a7716..b62fd4e0aad247c49586bb1d1acf264dfb636d5a 100644
--- a/generator/graph/PreciseSystemState.py
+++ b/generator/graph/PreciseSystemState.py
@@ -14,10 +14,12 @@ class PreciseSystemState(SystemState):
size = len(self.system_graph.subtasks)
- self.continuations = [None] * size
+ delattr(self, "events_cleared")
+ delattr(self, "events_set")
+
self.events = [0] * size
- self.call_stack = [None] * size
for i in range(0, size):
+ self.continuations[i] = None
self.call_stack[i] = list()
self.__hash = None
@@ -79,6 +81,11 @@ class PreciseSystemState(SystemState):
return self.call_stack[subtask.subtask_id]
# Events
+ def get_events(self, subtask):
+ """Return a tuple (None, set)"""
+ events = self.events[subtask.subtask_id]
+ return (subtask.event_mask_valid ^ events, events)
+
def set_events(self, subtask, event_list):
mask = Event.combine_event_masks(event_list)
self.events[subtask.subtask_id] |= mask
diff --git a/generator/graph/Subtask.py b/generator/graph/Subtask.py
index dd9ee5ae9af3be35042086248665c50c2c988af4..6f11ce8ff4e4c7d7dc71b975ac66a69186db4d03 100644
--- a/generator/graph/Subtask.py
+++ b/generator/graph/Subtask.py
@@ -16,6 +16,8 @@ class Subtask(Function, SystemObject):
self.task = None
self.subtask = self
self._events = {}
+ # A mask that is the combination of all event masks
+ self.event_mask_valid = 0
def find(self, cls, name):
if issubclass(cls, Event):
diff --git a/generator/graph/SystemGraph.py b/generator/graph/SystemGraph.py
index 1821dd3efc0b6d53d93062e044c7ef7cb1ab6812..b3b5b75a381ece1825fd866b78f08318ee7d855a 100644
--- a/generator/graph/SystemGraph.py
+++ b/generator/graph/SystemGraph.py
@@ -200,6 +200,7 @@ class SystemGraph(GraphObject, PassManager):
event.used = True
E = Event(self, "%s__%s"% (subtask.name, event.name), subtask, event_id, event)
subtask._events[event.name] = E
+ subtask.event_mask_valid |= E.event_mask
self._events[E.name] = E
event_id += 1
assert event_id < 32, "No more than 32 Events per Subtask"
diff --git a/generator/graph/SystemState.py b/generator/graph/SystemState.py
index a12e7b9e68e758df6281966b6622419c45ce0810..f11c2af90b7bb6fdbf6976a223aec5d33577ef1f 100644
--- a/generator/graph/SystemState.py
+++ b/generator/graph/SystemState.py
@@ -20,13 +20,18 @@ class SystemState(Node):
Node.__init__(self, Edge, "", color="green")
self.system_graph = system_graph
self.frozen = False
- self.states = []
- self.continuations = []
- self.call_stack = []
- for subtask in self.system_graph.subtasks:
- self.states.append(0)
- self.continuations.append(set())
- self.call_stack.append(None)
+
+ size = len(self.system_graph.subtasks)
+
+ self.states = [0] * size
+ self.continuations = [None] * size
+ self.events_cleared = [0] * size
+ self.events_set = [0] * size
+ self.call_stack = [None] * size
+
+ for i in range(0, size):
+ self.continuations[i] = set()
+
self.current_abb = None
self.__hash = None
@@ -109,6 +114,17 @@ class SystemState(Node):
analysis, which does not support events."""
pass
+ def get_events(self, subtask):
+ """Returns two bitmasks: (Event is cleared, Event is set)"""
+ return (self.events_cleared[subtask.subtask_id],
+ self.events_set[subtask.subtask_id])
+
+ def is_event_set(self, subtask, event):
+ return (self.events_set[subtask.subtask_id] & event.event_mask) != 0
+
+ def is_event_cleared(self, subtask, event):
+ return (self.events_cleared[subtask.subtask_id] & event.event_mask) != 0
+
## Continuations
def get_continuations(self, subtask):
if type(subtask) == int:
@@ -204,9 +220,13 @@ class SystemState(Node):
"%s != %s" %(self.current_abb.path(), other.current_abb.path())
self.current_abb = other.current_abb
changed = False
- for subtask_id in range(0, Subtask.subtask_id_counter):
+
+ for subtask in self.system_graph.subtasks:
+ subtask_id = subtask.subtask_id
+
old_state = self.states[subtask_id]
continuations_count = len(self.continuations[subtask_id])
+
self.states[subtask_id] |= other.states[subtask_id]
self.continuations[subtask_id] |= other.get_continuations(subtask_id)
# Check whether one set has changed
@@ -217,6 +237,14 @@ class SystemState(Node):
# We cannot merge call stacks!
self.call_stack[subtask_id] = None
+
+ # Merge Event masks
+ # FIXME: Events do not influence the changed flag correctly
+ (events_cleared, events_set) = other.get_events(subtask)
+ self.events_cleared[subtask_id] |= events_cleared
+ self.events_set[subtask_id] |= events_set
+
+
return changed
@staticmethod
diff --git a/generator/rules/syscalls_full.py b/generator/rules/syscalls_full.py
index 07fd8661feea763a84c9bcbe0d25d675d00f4434..f8f1c63737c0e3fb40cb70bbe6418f296047b971 100644
--- a/generator/rules/syscalls_full.py
+++ b/generator/rules/syscalls_full.py
@@ -246,11 +246,18 @@ class FullSystemCalls(BaseRules):
should_equal_zero = []
should_unequal_zero = []
for a in assertions:
- (equal_zero, cond) = self.__do_assertion(a)
- if equal_zero:
- should_equal_zero.append(cond)
+ x = self.__do_assertion(a)
+ if type(x[0]) == bool:
+ assertions = [x]
else:
- should_unequal_zero.append(cond)
+ (assertions, prepare) = x
+ block.add(prepare)
+
+ for equal_zero, cond in assertions:
+ if equal_zero:
+ should_equal_zero.append(cond)
+ else:
+ should_unequal_zero.append(cond)
call_hook = Statement("CALL_HOOK(FaultDetectedHook, STATE_ASSERTdetected, __LINE__, 0)")
if should_equal_zero:
@@ -265,6 +272,7 @@ class FullSystemCalls(BaseRules):
def __do_assertion(self, assertion):
task = assertion.get_arguments()[0]
+
if assertion.isA(AssertionType.TaskIsSuspended):
cond = "scheduler_.isReady(%s)" % self.task_desc(task)
return (True, cond)
@@ -277,5 +285,28 @@ class FullSystemCalls(BaseRules):
elif assertion.isA(AssertionType.TaskWasNotKickoffed):
cond = "%s.tcb.is_running()" % self.task_desc(task)
return (True, cond)
+ elif assertion.isA(AssertionType.EventsCheck):
+ event_cleared = assertion.get_arguments()[1]
+ event_set = assertion.get_arguments()[2]
+ var = "event_mask_%s" % task.name
+ prepare = Statement("uint32_t {var} = scheduler_.GetEvent_impl({task}); kout << \"{task}\"<< {var} << endl".format(
+ task = self.task_desc(task), var = var))
+ conds = []
+ if event_cleared:
+ # Mask Should equal to zero
+ mask = Event.combine_event_masks(event_cleared)
+ conds.append((True, "({var} & {mask})".format(var=var, mask=mask)))
+ if event_set:
+ # Mask Should equal to zero
+ mask = Event.combine_event_masks(event_set)
+ conds.append((True, "(({var} & {mask}) ^ {mask})".format(var=var, mask=mask)))
+
+ return (conds, prepare)
+ elif assertion.isA(AssertionType.EventsCleared):
+ cond = "(scheduler_.GetEvent_impt({task}) & {mask}) == 0".format(
+ task = self.task_desc(event_list[0].subtask),
+ mask = Event.combine_event_masks(event_list)
+ )
+ return (True, cond)
else:
- panic("Unsupported assert type %s in %s", assertion, block)
+ panic("Unsupported assert type %s", assertion)
diff --git a/os/scheduler/events-encoded.h b/os/scheduler/events-encoded.h
index 7ebf68968fd60c76a2b3b54047a144d52b582df2..c45343223c4d3930b6e01b9dcaf6a075c5e1cfcb 100644
--- a/os/scheduler/events-encoded.h
+++ b/os/scheduler/events-encoded.h
@@ -51,6 +51,10 @@ public:
event_set = EC(B1, High);
}
+ bool get() {
+ return (event_set.vc == EC(B1, High).vc);
+ }
+
void wait() {
event_waiting = EC(B0, High);
}
diff --git a/os/scheduler/scheduler-unencoded.h.in b/os/scheduler/scheduler-unencoded.h.in
index 352eac2b686e983f5d68e41499a3262f34de3386..1016d8c4e9d337179aa7c73ff6f9ee5386633015 100644
--- a/os/scheduler/scheduler-unencoded.h.in
+++ b/os/scheduler/scheduler-unencoded.h.in
@@ -81,7 +81,9 @@ struct Scheduler {
tlist.clear_events(current_task.id, event_mask);
}
-
+ forceinline uint32_t GetEvent_impl(const Task ¤t_task) {
+ return tlist.get_events(current_task.id);
+ }
forceinline void SetReadyFromSuspended_impl(const Task &task) {
SetPriority(task, task.prio);
diff --git a/os/scheduler/scheduler.h.in b/os/scheduler/scheduler.h.in
index 9073cca131628f6f6ce981ce68f02638475946f2..188af4c7ff584bbea53bdf3685cca8c4a78d040d 100644
--- a/os/scheduler/scheduler.h.in
+++ b/os/scheduler/scheduler.h.in
@@ -117,6 +117,9 @@ struct Scheduler {
forceinline void ClearEvent_impl(const Task ¤t_task, const int event_mask) {
tlist.clear_events(current_task.id, event_mask);
}
+ forceinline uint32_t GetEvent_impl(const Task ¤t_task) {
+ return tlist.get_events(current_task.id);
+ }
forceinline void SetPriority(const Task &task, const int new_prio) {
auto new_prio_encoded = EC(2, new_prio);
diff --git a/os/scheduler/tasklist-unencoded.h.in b/os/scheduler/tasklist-unencoded.h.in
index 0d8e7eb2512ff666939313a8523aab78976d7437..e78da95a91ae254e0e6e783a5fac2fd07a5d7dd9 100644
--- a/os/scheduler/tasklist-unencoded.h.in
+++ b/os/scheduler/tasklist-unencoded.h.in
@@ -143,6 +143,21 @@ struct TaskList : public UnencodedTaskListStatic {
forceinline void remove(const id_t& id) {
set(id, 0);
}
+
+ /** Get Events **/
+ forceinline event_mask_t get_events(const id_t id) {
+ (void) id;
+{{{!foreach_subtask|\
+ if (id == {{{!subtask_id}}}) {
+{{{!if_events|
+ return {{{!subtask}}}_events_set;
+}}}
+ } else \
+}}} {
+ }
+ return 0;
+ }
+
};
/** Equality operator (used for TMR) [enc=0] **/
diff --git a/os/scheduler/tasklist.h.in b/os/scheduler/tasklist.h.in
index 7582ae41d5ff0de9fb8cd5d60e5c58afed86d070..9d62975beae47189ce96d24457ab59691fe22cb6 100644
--- a/os/scheduler/tasklist.h.in
+++ b/os/scheduler/tasklist.h.in
@@ -239,6 +239,23 @@ struct TaskList : public TaskListStatic {
}
}
+ /** Get Events **/
+ forceinline event_mask_t get_events(const id_t id) {
+ (void) id;
+ event_mask_t ret = 0;
+{{{!foreach_subtask|\
+ if (id == {{{!subtask_id}}}) {
+{{{!foreach_event|
+ if ({{{!event}}}.get()) ret |= {{{!event_mask}}};
+}}}
+ } else \
+}}} {
+ }
+ return ret;
+ }
+
+
+
};
/** Equality operator (used for TMR) [enc=1] **/