FreeRTOS-Kernel
FreeRTOS-Kernel copied to clipboard
FreeRTOS
Arraylist task queue
Arraylist task queue
Description
Gives an array-back implementation of lists. The new implementation does not modify the list interface.
Test Steps
Runs with CBMC proofs. Have not tried to compile the kernel.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Is this intended for use with CBMC only, or for inclusion in release versions of the kernel?
Is this intended for use with CBMC only, or for inclusion in release versions of the kernel?
It is not CBMC-use only. This PR include an array-based implementation of lists with unbounded memory safety proof. With this PR along with the proofs, we want to make the array-based implementation more visible, and let people recognize the cost and the benefit of moving from linked-list to array-list so that they can have better idea about whether to move to array-list and what should be done before moving to array-list. We also want to see if there is any compatibility issue caused by the array-based implementation.
