Tobias Reinhard
|
60f1530d17
|
Deleted deprecated files.
|
2022-12-09 14:52:35 -05:00 |
|
Tobias Reinhard
|
21992b6c34
|
Startup script expects paths to relevant directories as arguments instead of computing them itself.
|
2022-12-09 14:51:00 -05:00 |
|
Tobias Reinhard
|
1d3fcdfc1f
|
Reverted modified source and header files to last commit before we started the VeriFast proofs.
Files reset to commit 13f034eb74
|
2022-12-09 10:37:50 -05:00 |
|
Tobias Reinhard
|
dcbaf3863b
|
Preprocessing script prefers modified files in proof subdirectory over files in main source and header dir.
|
2022-12-09 10:35:20 -05:00 |
|
Tobias Reinhard
|
cc7ed1e3eb
|
Copied modified source and header files to proof subdirectory.
|
2022-12-09 10:34:19 -05:00 |
|
Tobias Reinhard
|
2e78ed5884
|
Renamed VeriFast proof direcotry to comply with structure of main FreeRTOS repository.
|
2022-12-09 09:47:27 -05:00 |
|
Tobias Reinhard
|
eef76ea839
|
Simplified invariants.
|
2022-12-08 08:49:59 -05:00 |
|
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
|
9a81e7b860
|
Reordered verifast args in startup script to not only support the IDE but also the command line tool.
|
2022-12-06 13:00:05 -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
|
e68b45969b
|
Refined precondition of reordering lemma.
|
2022-12-06 09:54:03 -05:00 |
|
Tobias Reinhard
|
7fe2ec22f2
|
Strengthened postcondition of reordering lemma.
|
2022-12-06 09:24:08 -05:00 |
|
Tobias Reinhard
|
d028b1d04a
|
Added lemma to reason about reordering of ready lists.
|
2022-12-06 09:17:17 -05:00 |
|
Tobias Reinhard
|
4ac0f5e4ce
|
Added lemma to close reordered ready lists.
|
2022-12-05 15:52:01 -05:00 |
|
Tobias Reinhard
|
ee2922ad80
|
Finished some proof branches in prvSelectHighestPriorityTask.
|
2022-12-05 14:46:11 -05:00 |
|
Tobias Reinhard
|
346a7f778a
|
Added lemma to close ready lists predicate.
|
2022-12-05 14:40:01 -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
|
1919f8142f
|
Deleted deprecated lemmas and predicates.
|
2022-12-02 15:07:43 -05:00 |
|
Tobias Reinhard
|
3be9d76d82
|
Made sharedSeg_TCB_p precise to allow merging of fractions without opening and closing
|
2022-12-02 15:06:25 -05:00 |
|
Tobias Reinhard
|
b44eb855d9
|
Deleted deprecated predicate and lemmas.
|
2022-12-02 15:05:20 -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
|
eb1cfa53d3
|
Exposed running state macros to VF.
|
2022-12-02 11:54:12 -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
|
9b2bb08cb5
|
Extended precondition of vListInsertEnd to prove absence of overflows.
|
2022-12-01 14:57:13 -05:00 |
|
Tobias Reinhard
|
8976bd4d03
|
Adapted single-core proof of vListInitialise to new version of predicates.
|
2022-12-01 14:49:19 -05:00 |
|
Tobias Reinhard
|
0633baba2f
|
Added single-core proof for vListInsertEnd by Aalok Thakkar and Nathan Chong.
|
2022-12-01 12:54:52 -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
|
6f782b494a
|
VF start script takes font size as 2nd param
|
2022-12-01 08:01:05 -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
|
70f1041778
|
Added documentation.
|
2022-11-29 15:55:27 -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
|
b310efa029
|
Added ready list lemmas.
|
2022-11-29 08:32:32 -05:00 |
|
Tobias Reinhard
|
2048fb85da
|
Commented old opening and closing lemmas out and switched back from Z3 to VF standard SMT solver
|
2022-11-28 12:20:30 -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
|
bb00bee690
|
Finished proof of DLS_close_2.
|
2022-11-28 09:16:08 -05:00 |
|