43defa566c
* Update History.txt and README.md for December release (#744) * Update History.txt and README.md for release * Bump mbedtls submodule to v2.28.0 (#745) * Patch project files for mbedtls (#751) * Apply group 1 patches * Apply patches for group 2 * Update project files for mbedTLS new version Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> * Fix warnings in projects Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> * Fix warnings in HTTP_S3_Download demo Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com> Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com> * Update changelog and history for corePKCS11 update (#752) * Update submodule pointer and manifest.yml for corePKCS11 (#754) * Update readme and history.txt to show that Sigv4 is a newly added library (#756) * Revert update to v143 of VS toolset (#757) * [AUTO][RELEASE]: Bump file header version to "202112.00" * Update file headers to satisfy core checks Co-authored-by: Muneeb Ahmed <54290492+muneebahmed10@users.noreply.github.com> Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com> Co-authored-by: johnrhen <johnrhen@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| listLIST_IS_EMPTY.c | ||
| README.md | ||
| uxListRemove.c | ||
| vListInitialise.c | ||
| vListInitialiseItem.c | ||
| vListInsert.c | ||
| vListInsertEnd.c | ||
FreeRTOS list proofs
The list predicates and proofs are inspired by and based on the work from Ferreira et al. (STTT'14).
The main shape predicate is a doubly-linked list segment (DLS), as defined
by Ferreira et al. in Fig 15. A DLS is defined by two xLIST_ITEM struct
pointers n and m (possibly pointing to the same item) which are the start
and end of the segment. We track the item pointers and values within the DLS in
the lists cells and vals, respectively. Therefore n and m are the first
and last items of cells.
+--+ +--+
-----n-> |*n| ... |*m| -mnext->
<-nprev- | | | | <-m-----
+--+ +--+
^-----------^
DLS(n, nprev, mnext, m)
With base case: n == m (single item case)
+--+
-----n-> |*n| -mnext->
<-nprev- | | <-n-----
+--+
^--^
xLIST_ITEM
DLS(n, nprev, mnext, n)
Cons case:
+--+ +--+ +--+
-----n-> |*n| -o-> |*o| ... |*m| -mnext->
<-nprev- | | <-n- | | | | <-m-----
+--+ +--+ +--+
^--^ ^-----------^
xLIST_ITEM DLS(o, n, mnext, m)
^---------------------^
DLS(n, nprev, mnext, m)
A DLS can be made into a well-formed list by joining n and m into a cycle.
Note that unlike Ferreira et al.'s list shape predicate, we always start with
the sentinel end item to avoid a top-level case-split. So in the following
diagram the start and end of the DLS are end and the item-before-end
endprev.
.-----------------------------------.
| +--------+ +--------+ |
`--> |*end | ... |*endprev| ----'
.---- | | | | <---.
| +--------+ +--------+ |
`----------------------------------'
^-----------------------^
DLS(end, endprev, end, endprev)
References
- Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK
João F. Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin
https://joaoff.com/publication/2014/sttt/