mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-12-12 06:35:19 -05:00
55 lines
2.1 KiB
Markdown
55 lines
2.1 KiB
Markdown
This directory contains the bulk of VeriFast formalizations and proofs.
|
|
|
|
|
|
# Directory Structure
|
|
```
|
|
├── lock_predicates.h
|
|
│ Contains the formalization of the lock invariants, i.e., the invariants
|
|
│ associated with: Masking interrupts, the task lock and the ISR lock.
|
|
│ This file also contains the lemmas to prove that the task state updates
|
|
│ in `prvSelectHighestPriorityTask` preserve the lock invariants.
|
|
│
|
|
├── port_contracts.h
|
|
│ Contains VeriFast function contracts for macros with port-specific
|
|
│ definitions, e.g., the macros to mask interrupts and to acquire AND
|
|
│ release locks. These port-specific definitions often contain contain
|
|
│ inline assembly VeriFast cannot reason about. The contracts allow us
|
|
│ to abstract the semantics of the assembly.
|
|
│
|
|
├── ready_list_predicates.h
|
|
│ Contains the predicates describing the ready lists as well as lemmas to
|
|
│ reason about ready lists.
|
|
│
|
|
├── stack_predicates.h
|
|
│ Contains the formalization of the stack layout used in the RP2040 port.
|
|
│
|
|
├── task_predicates.h
|
|
│ Contains predicates describing task control blocks.
|
|
│
|
|
├── task_running_states.h
|
|
│ `tasks.c` defines macros that are used to denote task run states.
|
|
│ The proof headers in this directory cannot refer to these macros.
|
|
│ This header contains auxiliary definitions used to expose the run state
|
|
│ macros to the proof headers.
|
|
│
|
|
├── verifast_lists_extended.h
|
|
│ Contains list axioms and lemmas that would naturally fit into VeriFast's
|
|
│ standard list library `listex.gh`.
|
|
│
|
|
├── README.md
|
|
│
|
|
├── single_core_proofs
|
|
│ Contains the old list formalization and proofs written by
|
|
│ Aalok Thakkar and Nathan Chong in 2020 for the single-core
|
|
│ setup.
|
|
│ │
|
|
│ ├── scp_common.h
|
|
│ │ Contains auxiliary definitions and lemmas.
|
|
│ │
|
|
│ └── scp_list_predicates.h
|
|
│ Contains the formalizaton of doubly linked lists and list items.
|
|
│
|
|
└── single_core_proofs_extended
|
|
Contains new proofs extending the single-core list
|
|
formalization.
|
|
```
|