Tobias Reinhard
|
99d46f9e51
|
Guarded unsafe decrements of uxTopReadyPriority and uxCurrentPriority
|
2022-12-08 08:45:17 -05:00 |
|
Tobias Reinhard
|
136b1d69b2
|
Updated ready list invariant from requiring exactly 1 idle task to configNUM_CORES idle tasks.
|
2022-12-07 07:34:46 -05:00 |
|
Tobias Reinhard
|
f98779f0cb
|
Finished proof branch dealing with ready list reordering. Strict positivity of uxCurrentPriority remains to be proven.
|
2022-12-06 10:16:22 -05:00 |
|
Tobias Reinhard
|
ee2922ad80
|
Finished some proof branches in prvSelectHighestPriorityTask.
|
2022-12-05 14:46:11 -05:00 |
|
Tobias Reinhard
|
e71756e4cb
|
Proved that decrementing uxTopReadyPriority does not lead to underflow.
|
2022-12-04 13:46:32 -05:00 |
|
Tobias Reinhard
|
00bb9d4a17
|
Verified runtime assertion that running task is either scheduled or yielding.
|
2022-12-04 11:54:07 -05:00 |
|
Tobias Reinhard
|
61bffc4617
|
Adapted loop invariant to reflect potential change of state lists.
|
2022-12-04 10:46:05 -05:00 |
|
Tobias Reinhard
|
b594404b59
|
Restored loop invariant at end of task-swapping branch
|
2022-12-04 10:33:36 -05:00 |
|
Tobias Reinhard
|
fbf4ba981f
|
Added lemmas to update read permissions for unscheduled tasks after new task has been started.
|
2022-12-04 10:19:48 -05:00 |
|
Tobias Reinhard
|
6a0b2116fe
|
Added lemmas to define updated state lists and reason locally about results. Local reasoning necessary to avoid auto-lemma application loops.
|
2022-12-04 09:17:13 -05:00 |
|
Tobias Reinhard
|
e403e8bc74
|
Added lemma to update the read permissions for unscheduled tasks after a task has been stopped.
|
2022-12-03 18:05:15 -05:00 |
|
Tobias Reinhard
|
0df45b465e
|
Added lemmas that allow updating the lock invariant after a state update.
|
2022-12-03 14:54:26 -05:00 |
|
Tobias Reinhard
|
dda2dbda6f
|
Added states list to lock invariant.
|
2022-12-03 10:04:04 -05:00 |
|
Tobias Reinhard
|
e4db1f8aba
|
Refined lock invariant to only give read permission to all tasks and write permission to locally scheduled task
|
2022-12-03 08:58:19 -05:00 |
|
Tobias Reinhard
|
df780a1823
|
Introduced list of flat list of tasks in lock invariant. Simplifies access to sharedSeg_TCB_p chunks.
|
2022-12-02 14:59:06 -05:00 |
|
Tobias Reinhard
|
2c6d35943f
|
Update tasks.c
Restored loop invariant at end of inner loop.
|
2022-12-01 15:08:43 -05:00 |
|
Tobias Reinhard
|
122ecdeac0
|
Proved that call to uxListRemove in prvSelectHighestPriorityTaskis safe.
|
2022-12-01 12:48:43 -05:00 |
|
Tobias Reinhard
|
cd3fa4e577
|
Added adaptation of Aalok's and Nathan's single-core proof for uxListRemove
|
2022-12-01 11:47:52 -05:00 |
|
Tobias Reinhard
|
fe5612cf4f
|
Extended lock invariants to justify safe access to ready tasks as well as scheduled task.
|
2022-11-30 15:52:00 -05:00 |
|
Tobias Reinhard
|
78de786d89
|
Expanded lock invariant to give us access to shared segments of all ready TCBs.
|
2022-11-30 11:05:06 -05:00 |
|
Tobias Reinhard
|
e800ebd293
|
Exposed node owners in all predicates related to nodes. Adapted proofs to new predicates.
Changed predicates:
- `xLIST_ITEM`
- `DLS`
- `xLIST`
- `readyLists_p`
- `List_array_p`
|
2022-11-30 09:44:25 -05:00 |
|
Tobias Reinhard
|
22dc5c1287
|
Added proof idea and TODOs. Need to refactor single-core list predicates.
|
2022-11-29 13:53:53 -05:00 |
|
Tobias Reinhard
|
e8b8234416
|
Renamed predicates to comply with naming conventions
|
2022-11-29 09:47:50 -05:00 |
|
Tobias Reinhard
|
014acb9a00
|
Refactored lock predicates to improve readability.
|
2022-11-29 09:37:23 -05:00 |
|
Tobias Reinhard
|
c0df2a2894
|
Adapted proof of prvSelectHighestPriorityTask to use new DLS representation and opening & closing lemmas.
|
2022-11-28 10:55:39 -05:00 |
|
Tobias Reinhard
|
53189c46d4
|
Added new version of DLS opening lemma that reduces case splits in DLS proofs. Proved 3/4 of it.
|
2022-11-26 12:15:34 -05:00 |
|
Tobias Reinhard
|
49af8fd30f
|
Finished verification of iteration updates in prvSelectHighestPriorityTask.
|
2022-11-23 15:18:11 -05:00 |
|
Tobias Reinhard
|
9d1b47c5e5
|
Added lemmas to simplify opening and closing DLS for cases of the form pxTask->pxNext
|
2022-11-23 13:53:10 -05:00 |
|
Tobias Reinhard
|
f44473b47c
|
Applied closing lemmas.
|
2022-11-23 11:34:47 -05:00 |
|
Tobias Reinhard
|
397cb12abb
|
Added lemmas to reason about updates to pointers in the ready list of the form pxTaskItem = pxTaskItem->pxNext
|
2022-11-22 13:08:22 -05:00 |
|
Tobias Reinhard
|
538f29caeb
|
Closed some predicates to simplify proof state.
|
2022-11-22 10:17:37 -05:00 |
|
Tobias Reinhard
|
f7e537a19f
|
Restructured proof.
New proof opens the DLS predicate to justify accesses to `pxTaskItem->next` and proves that `pxTaskItem->next` points to a valid list item.
|
2022-11-22 10:10:41 -05:00 |
|
Tobias Reinhard
|
49643b6f5e
|
Partial proof justifying that updates of pxTaskItem in inner search loop in prvSelectHighestPriorityTask are safe.
|
2022-11-22 07:18:45 -05:00 |
|
Tobias Reinhard
|
35aef80072
|
Proved that pxTaskItem points to valid list item before inner search loop.
|
2022-11-21 14:02:23 -05:00 |
|
Tobias Reinhard
|
de3657239f
|
Added minimal loop invariant to inner search loop in prvSelectHighestPriorityTask.
|
2022-11-21 11:32:25 -05:00 |
|
Tobias Reinhard
|
92a925bb59
|
Verified selection of initial task item in search loop in prvSelectHighestPriorityTask.
|
2022-11-21 09:45:22 -05:00 |
|
Tobias Reinhard
|
cf65065a0c
|
Used single-core list predicate xLIST to express access permissions to ready lists in readyLists_p.
|
2022-11-18 16:27:38 -05:00 |
|
Tobias Reinhard
|
1888670656
|
Removed unneeded precondition
|
2022-11-18 13:35:06 -05:00 |
|
Tobias Reinhard
|
e629319b9f
|
Relaxed contract of xTaskGetCurrentTaskHandle.
|
2022-11-18 09:32:24 -05:00 |
|
Tobias Reinhard
|
c9e61fce49
|
Introduced initial formulation of predicate to capture shared ready lists.
|
2022-11-18 09:22:31 -05:00 |
|
Tobias Reinhard
|
6dcaef48d6
|
Added loop invariant to main search loop in prvSelectHighestPriorityTask.
|
2022-11-17 14:24:44 -05:00 |
|
Tobias Reinhard
|
9b2871bc92
|
Formulated first version of contract for prvSelectHighestPriorityTask and adapted proof of vTaskSwitchContext accordingly.
|
2022-11-17 12:55:01 -05:00 |
|
Tobias Reinhard
|
fb01980b63
|
Verified new contract for xTaskGetCurrentTaskHandle.
|
2022-11-17 12:08:38 -05:00 |
|
Tobias Reinhard
|
63a8d73ecc
|
Apdated proof for vTaskSwitchContext to rely on the proof of taskCHECK_FOR_STACK_OVERFLOW
|
2022-11-17 10:23:39 -05:00 |
|
Tobias Reinhard
|
d3bda01f16
|
Verified macro taskCHECK_FOR_STACK_OVERFLOW.
|
2022-11-17 09:20:21 -05:00 |
|
Tobias Reinhard
|
2f0b8bc82f
|
Added proof steps outlining the verification of stack inspection. Also added TODOs concerning rewrites necessary for the verification of the macro.
|
2022-11-16 16:08:15 -05:00 |
|
Tobias Reinhard
|
c3c350f8dc
|
vTaskSwitchContext now has access to the current task's stack.
|
2022-11-16 15:31:49 -05:00 |
|
Tobias Reinhard
|
b330847935
|
Added preliminary post condition for vTaskSwitchContext
|
2022-11-16 14:26:37 -05:00 |
|
Tobias Reinhard
|
4eb2fa573e
|
Wrote contracts for lock release operations.
|
2022-11-16 14:18:03 -05:00 |
|
Tobias Reinhard
|
54523ecdce
|
Included global variables pxCurrentTCBs and pxYieldingPendings in interrupt invariant.
|
2022-11-16 13:53:22 -05:00 |
|