Tobias Reinhard
|
5cf8b4ed1c
|
Added shared global variable xSchedulerRunning to task-isr lock invariant.
|
2022-11-21 08:06:19 -05:00 |
|
Tobias Reinhard
|
81355bc42f
|
Added DLS lemmas related tosplit.
|
2022-11-21 08:05:32 -05:00 |
|
Tobias Reinhard
|
5b6a92f023
|
Added TODO
|
2022-11-18 16:47:47 -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
|
8f463be9d8
|
VF rewrite: Changed type of List_t.xListEnd to match expectations of single-core list proofs.
|
2022-11-18 15:39:41 -05:00 |
|
Tobias Reinhard
|
b1fc658413
|
Added single-core list predicates and proofs. Most proofs are commented out for the moment.
|
2022-11-18 15:38:32 -05:00 |
|
Tobias Reinhard
|
f5c0a64f86
|
Made isr lock predicate abstract.
|
2022-11-18 14:31:37 -05:00 |
|
Tobias Reinhard
|
02e019fe45
|
Highlighted that reused list proofs assume single-core setting.
|
2022-11-18 13:46:43 -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
|
a7d1ca343a
|
VF rewrite: Fixed an evaluation order in taskCHECK_FOR_STACK_OVERFLOW.
|
2022-11-16 15:50:09 -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
|
383a055872
|
taskCHECK_FOR_STACK_OVERFLOW assumes minimal stack size. Updated stack predicate accordingly.
|
2022-11-16 15:30:40 -05:00 |
|
Tobias Reinhard
|
7675b3bbe4
|
Rewrote macro taskCHECK_FOR_STACK_OVERFLOW such that VF can handle it.
|
2022-11-16 15:28:33 -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 |
|
Tobias Reinhard
|
d63a8f83cd
|
Renamed predicate encapsulating access permissions to core local variables to coreLocalInterruptInv_p.
|
2022-11-16 11:31:12 -05:00 |
|
Tobias Reinhard
|
327423ef67
|
TCB of currently scheduled task on core C is interrupt protected on core C. Updated invariants to reflect that.
|
2022-11-16 11:25:37 -05:00 |
|
Tobias Reinhard
|
dbf03a0ab2
|
Introduced predicates to differentiate between public and private parts of a TCB.
|
2022-11-16 10:55:25 -05:00 |
|
Tobias Reinhard
|
360afe4374
|
Cleaned up lock predicate header.
|
2022-11-16 10:37:12 -05:00 |
|
Tobias Reinhard
|
d95976ebe5
|
Added info about available tasks to lock predicate.
|
2022-11-16 10:28:31 -05:00 |
|
Tobias Reinhard
|
7a5119e324
|
Nightly build of Nov 14, 2022 broke old proof for vTaskCreate. Ignoring these proofs for now.
|
2022-11-15 09:31:56 -05:00 |
|
Tobias Reinhard
|
d2f10a6b25
|
vTaskSwitchContexxt assumes that that interrupts have been deactivated.
|
2022-11-15 08:28:21 -05:00 |
|
Tobias Reinhard
|
a7fdaca373
|
Reverted manual rewrites involving const pointers. Automatic rewrites are in place.
|
2022-11-13 14:52:14 -05:00 |
|
Tobias Reinhard
|
a470fec6d0
|
Added automatic deletion of void casts (used to suppress warnings) and linked to filed VeriFast issue 335.
|
2022-11-13 14:46:17 -05:00 |
|
Tobias Reinhard
|
1e2acf6139
|
Linked const pointer rewrite to filed VeriFast issue 333.
|
2022-11-13 14:35:02 -05:00 |
|
Tobias Reinhard
|
7c9711cb88
|
Reverted manual VF rewrites concerning const pointers. Respective rewrites are applied during preprocessing.
|
2022-11-11 15:44:23 -05:00 |
|
Tobias Reinhard
|
0a31349be3
|
Added automatic rewrite to remove const qualifiers occurring before a star.
|
2022-11-11 15:37:24 -05:00 |
|
Tobias Reinhard
|
49f0dc1f04
|
Added preprocessing out dir to .gitignore.
|
2022-11-11 15:11:44 -05:00 |
|
Tobias Reinhard
|
e33d940357
|
Stopped tracking preprocecssing output.
|
2022-11-11 15:09:27 -05:00 |
|
Tobias Reinhard
|
d746a27233
|
Added missing task-ISR lock invariant to post condition of acquision lemma.
|
2022-11-11 15:07:01 -05:00 |
|
Tobias Reinhard
|
29e14be203
|
Verified minimal contract for xTaskGetCurrentTaskHandle.
|
2022-11-10 14:36:04 -05:00 |
|
Tobias Reinhard
|
63d8c5afa8
|
Rewrote side-effectful assertion such that VeriFast can process it.
|
2022-11-10 12:51:20 -05:00 |
|
Tobias Reinhard
|
7e75d7aa8f
|
Refined lock predicates and contracts for lock macros to match expected locking discipline.
|
2022-11-10 12:50:48 -05:00 |
|
Tobias Reinhard
|
3d4ad64692
|
Switched to new verification target vTaskSwitchContext.
|
2022-11-07 14:42:11 -05:00 |
|
Tobias Reinhard
|
9fa8c76447
|
Paused partial proof for xTaskCreate.
|
2022-11-07 14:40:08 -05:00 |
|
Tobias Reinhard
|
c4f5c09a81
|
Altered config to ensure that we don't accidentally rely on a concrete small number of cores.
|
2022-11-07 14:34:54 -05:00 |
|
Tobias Reinhard
|
91eb6eefaa
|
Included reference to core ID in interrupt predicates and added distinction between global and core local variables.
|
2022-11-07 14:21:42 -05:00 |
|
Tobias Reinhard
|
06d2611aa9
|
Made config macros from FreeRTOSConfig.h available to VeriFast proof.
|
2022-11-04 16:16:08 -04:00 |
|
Tobias Reinhard
|
8897e3fe6e
|
Added specification for enabling and disabling interrupts.
|
2022-11-04 15:49:24 -04:00 |
|
Tobias Reinhard
|
66d71c5b47
|
Started to verify taskENTER_CRITICAL.
|
2022-11-04 14:23:39 -04:00 |
|
Tobias Reinhard
|
1e4e650650
|
Removed duplicate macro definition.
|
2022-11-04 14:22:54 -04:00 |
|