Added lemmas that allow updating the lock invariant after a state update.

tasks.c

@@ -1051,6 +1051,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         mem(pxTaskItem, gCells) == true &*&
                         xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
                         gSize > 0 &*&
+                        exists_in_taskISRLockInv_p(gTasks, gStates)
+                        &*&
                         // Read permissions for every task
                             foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) 
                         &*&
@@ -1059,7 +1061,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         &*&
                         // TODO:
                         // Write permissions for unscheduled tasks
-                            true
+                            foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates))
                         &*&
                         subset(gOwners, gTasks) == true;
 
@@ -1107,10 +1109,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
                      @*/
                     //@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners);
 
-                    // Getting access to fields of `pxTCB`
+                    // Getting read access to fields of `pxTCB`
+                    // aka first half of write permission
                         //@ assert( subset(gOwners, gTasks) == true );
                         //@ mem_subset(pxTCB, gOwners, gTasks);
                         //@ foreach_remove(pxTCB, gTasks);
+                    //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
 
                     /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */
 
@@ -1139,17 +1143,64 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         {
                             //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
                             //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] );
-                            /*@
+                            //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) );
-                            if( gCurrentTCB == pxTCB ) {
+
-                                // We can use the opened `sharedSeg_TCB_p` chunk
+                            /* We could reuse the read permission to `pxTCB` we extracted before the if statement.
-                                // for `pxTCB`.
+                             * But putting permissions back as soon as we no longer need them simplifies the 
-                            } else {
+                             * proof state and elimintates case-splits in the proof.
-                                neq_mem_remove(gCurrentTCB, pxTCB, gTasks);
+                             */
-                                foreach_remove(gCurrentTCB, remove(pxTCB, gTasks));
+
-                            }
+                            // Put read permission for `pxTCB` back
+                                //@ close [1/2]sharedSeg_TCB_p(pxTCB, _);
+                                //@ close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB);
+                                //@ foreach_unremove(pxTCB, gTasks);
+                            //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
+
+                            // Get 2nd half of write permission for `gCurrentTCB`
+                                //@ foreach_remove(gCurrentTCB, gTasks);
+                            //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
+                
+                            //@ int gCurrentTCB_index = index_of(gCurrentTCB, gTasks);
+                            /*@ list<TaskRunning_t> gStates1 =  
+                                    update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates);
                              @*/
+
                             /* If the task is not being executed by any core swap it in */
                             pxCurrentTCBs[ xCoreID ]->xTaskRunState = taskTASK_NOT_RUNNING;
+
+                            //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
+
+                            //@ open exists_in_taskISRLockInv_p(gTasks, gStates);
+
+                            /*@ close_updated_foreach_readOnly_sharedSeg_TCB
+                                    (gCurrentTCB, gTasks, gStates,
+                                     gStates1, taskTASK_NOT_RUNNING);
+                             @*/
+
+//@ assume(false);
+                            /*@ list<TaskRunning_t> gStates2 = 
+                                update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates);
+                            @*/
+
+                            // If we acquired an additional second half of a
+                            // write permission for `gCurrentTCB`, release it.
+                                /*@
+                                if( gCurrentTCB == pxTCB ) {
+                                    // We used the opened `sharedSeg_TCB_p` chunk
+                                    // for `pxTCB`. 
+                                    // => We don't have to close anything.
+                                } else {
+                                    close sharedSeg_TCB_p(gCurrentTCB, taskTASK_NOT_RUNNING);
+                    assert( gCurrentTCB_index < length(gTasks) );
+                    assert( gCurrentTCB_index < length(gStates) );
+        //            nonauto_nth_update(gCurrentTCB_index, gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates);
+        //            assert( taskTASK_NOT_RUNNING == nth(gCurrentTCB_index, gStates2) );
+                    assume( taskTASK_NOT_RUNNING == nth(gCurrentTCB_index, gStates2) );
+                                    close readOnly_sharedSeg_TCB_p(gTasks, gStates2)(gCurrentTCB);
+                                    foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks));
+                                }
+                                @*/
+
                             #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) )
                                 pxPreviousTCB = pxCurrentTCBs[ xCoreID ];
                             #endif
@@ -1157,21 +1208,18 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             pxCurrentTCBs[ xCoreID ] = pxTCB;
                             xTaskScheduled = pdTRUE;
 
-                            /*@
+                            
-                            if( gCurrentTCB == pxTCB ) {
+                            
-                                // We used the opened `sharedSeg_TCB_p` chunk
+
-                                // for `pxTCB`. 
+                            
-                                // => We don't have to close anything.
+                            
-                            } else {
+                            // Release second half of write permission for `pxTCB`
-                                close sharedSeg_TCB_p(gCurrentTCB);
+                                //@ foreach_unremove(pxTCB, gTasks);
-                                close readOnly_sharedSeg_TCB_p(gCurrentTCB);
-                                foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks));
-                            }
-                            @*/
 
                             // Ensure we restored the collection as it was
                             // at the beginning of the block.
                             //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
+                            //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) );
                         }
                     }
                     else if( pxTCB == pxCurrentTCBs[ xCoreID ] )

verification/verifast/proof/verifast_lists_extended.h

@@ -121,6 +121,61 @@ ensures mem(x, remove(r, xs)) == (mem(x, xs) && x != r);
 fixpoint bool superset<t>(list<t> super, list<t> sub) {
     return subset(sub, super);
 }
+
+
+// TODO: Can we prove this in VeriFast or do we have to axiomatise?
+lemma void update_out_of_bounds<t>(int index, t x, list<t> xs)
+requires (index < 0 || index >= length(xs));
+ensures update(index, x, xs) == xs;
+{
+    switch(xs) {
+        case nil:   // nothing to do
+        case cons(h, rest): {
+            update_out_of_bounds(index-1, x, rest);
+        }
+    }
+}
+
+
+lemma void index_of_different<t>(t x1, t x2, list<t> xs)
+requires x1 != x2 &*& mem(x1, xs) == true &*& mem(x2, xs) == true;
+ensures index_of(x1, xs) != index_of(x2, xs);
+{
+    switch(xs) {
+        case nil: 
+        case cons(h, rest):
+            if(h != x1 && h != x2) {
+                index_of_different(x1, x2, rest);
+            }
+    }
+}
+
+// TODO: Can we prove this in VeriFast or do we have to axiomatise?
+lemma void subset_cons_tail<t>(list<t> xs);
+requires xs == cons(?h, ?t);
+ensures subset(t, xs) == true;
+
+// TODO: Can we prove this in VeriFast or do we have to axiomatise?
+lemma void remove_result_subset<t>(t x, list<t> xs);
+requires true;
+ensures subset(remove(x, xs), xs) == true;
+// TODO: Revisit this lemma
+// {
+//     switch(xs) {
+//         case nil: 
+//         case cons(h, t):
+//             remove_result_subset(x, t);
+//             if(h == x) {
+//                 assert( remove(x, xs) == t );
+//                 subset_cons_tail(xs);
+//                 assert( subset(t, cons(x, t) ) == true );
+//             } else {
+//                 ;
+//             }
+//     }
+// }
+
+
 @*/
 
 

verification/verifast/proof/verifast_lock_predicates.h

@@ -1,7 +1,7 @@
 #ifndef VERIFAST_LOCK_PREDICATES_H
 #define VERIFAST_LOCK_PREDICATES_H
 
-
+#include "verifast_task_running_states.h"
 
 
 /* We follow a minimalistic approach during the definition of the
@@ -11,7 +11,7 @@
  * other parts of FRTOS.
  */
 
-
+#include "verifast_lists_extended.h"
 
 
 
@@ -112,7 +112,9 @@ predicate taskISRLockInv_p() =
         // TODO:
         // (RP-Unsched) Read permissions for unscheduled tasks
         // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks
-            true
+        // ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING
+        //             -> [1/2]shared_TCB_p(t, taskTASK_NOT_RUNNING)
+            foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates))
         &*&
         readyLists_p(?gCellLists, ?gOwnerLists) 
         &*&
@@ -146,7 +148,8 @@ predicate exists_in_taskISRLockInv_p(list<void*> gTasks,
                                      list<TaskRunning_t> gStates) =
     exists(gTasks) &*&
     exists(gStates) &*&
-    length(gTasks) == length(gStates);
+    length(gTasks) == length(gStates) &*&
+    distinct(gTasks) == true;
 
 // Auxiliary function that allows us to partially apply the list argument.
 //
@@ -166,10 +169,125 @@ predicate_ctor readOnly_sharedSeg_TCB_p
             (TCB_t* t;) =
     mem(t, tasks) == true &*&
     [1/2]sharedSeg_TCB_p(t, nth(index_of(t, tasks), states));
+
+predicate_ctor readOnly_sharedSeg_TCB_IF_not_running_p
+            (list<void*> tasks, list<TaskRunning_t> states)
+            (TCB_t* t;) =
+    mem(t, tasks) == true &*&
+    nth(index_of(t, tasks), states) == taskTASK_NOT_RUNNING
+        ? [1/2]sharedSeg_TCB_p(t, taskTASK_NOT_RUNNING)
+        : true;
+@*/
+
+
+
+/*@
+lemma void nonauto_nth_update<t>(int i, int j, t y, list<t> xs);
+  requires 0 <= i && i < length(xs) && 0 <= j && j < length(xs);
+  ensures nth(i, update(j, y, xs)) == (i == j ? y : nth(i, xs));
+@*/
+
+
+
+/*@
+lemma void update_readOnly_sharedSeg_TCB(TCB_t* t, 
+                                         list<void*> tasks,
+                                         list<TaskRunning_t> states, 
+                                         int updatedIndex,
+                                         TaskRunning_t s)
+requires readOnly_sharedSeg_TCB_p(tasks, states)(t) &*&
+         updatedIndex != index_of(t, tasks) &*&
+         mem(t, tasks) == true &*&
+         length(tasks) == length(states);
+ensures  readOnly_sharedSeg_TCB_p(tasks, update(updatedIndex, s, states))(t);
+{
+    list<TaskRunning_t> states2 = update(updatedIndex, s, states);
+    int t_index = index_of(t, tasks);
+
+    if( updatedIndex < 0 || updatedIndex >= length(states) ) {
+        update_out_of_bounds(updatedIndex, s, states);
+    } else {
+        open readOnly_sharedSeg_TCB_p(tasks, states)(t);
+        open [1/2]sharedSeg_TCB_p(t, nth(t_index, states));
+
+        mem_index_of(t, tasks);
+        nth_update(t_index, updatedIndex, s, states);
+        assert( nth(t_index, states) == nth(t_index, states2) );
+
+        close [1/2]sharedSeg_TCB_p(t, nth(t_index, states2));
+        close readOnly_sharedSeg_TCB_p(tasks, states2)(t);
+    }
+}
+
+
+lemma void update_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, 
+                                                 list<void*> tasks,
+                                                 list<void*> subTasks,
+                                                 list<TaskRunning_t> states, 
+                                                 list<TaskRunning_t> states2, 
+                                                 TaskRunning_t s)
+requires
+    mem(updatedTask, tasks) == true &*&
+    length(tasks) == length(states) &*&
+    foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states)) &*&
+    states2 == update(index_of(updatedTask, tasks), s, states) &*&
+    distinct(tasks) == true &*&
+    mem(updatedTask, subTasks) == false &*&
+    subset(subTasks, tasks) == true;
+ensures
+    foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states2));
+{
+    switch(subTasks) {
+        case nil:   
+            open foreach(nil, readOnly_sharedSeg_TCB_p(tasks, states));
+            close foreach(nil, readOnly_sharedSeg_TCB_p(tasks, states2));
+        case cons(h, rest):
+            int index = index_of(updatedTask, tasks);
+//            distinct_mem_remove(t, tasks);
+//            neq_mem_remove(h, t, tasks);
+//            index_of_different(h, t, tasks);
+            open foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states));
+            assert( updatedTask != h );
+            index_of_different(updatedTask, h, tasks);
+            assert( index != index_of(h, tasks) );
+            update_readOnly_sharedSeg_TCB(h, tasks, states, index, s);
+            assert( mem(updatedTask, rest) == false );
+            update_foreach_readOnly_sharedSeg_TCB(updatedTask, tasks, rest, 
+                                                  states, states2, s);
+            close foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states2));
+    }
+}
+
+
+lemma void close_updated_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, 
+                                                        list<void*> tasks,
+                                                        list<TaskRunning_t> states, 
+                                                        list<TaskRunning_t> states2, 
+                                                        TaskRunning_t s)
+requires
+    mem(updatedTask, tasks) == true &*&
+    length(states) == length(tasks) &*&
+    distinct(tasks) == true &*&
+    foreach(remove(updatedTask, tasks), readOnly_sharedSeg_TCB_p(tasks, states)) &*&
+    states2 == update(index_of(updatedTask, tasks), s, states) &*&
+    [1/2]sharedSeg_TCB_p(updatedTask, s);
+ensures
+    foreach(tasks, readOnly_sharedSeg_TCB_p(tasks, states2));
+{
+    distinct_mem_remove(updatedTask, tasks);
+    remove_result_subset(updatedTask, tasks);
+
+    close readOnly_sharedSeg_TCB_p(tasks, states2)(updatedTask);
+    update_foreach_readOnly_sharedSeg_TCB(updatedTask, tasks, 
+                                          remove(updatedTask, tasks),
+                                          states, states2, s);
+    foreach_unremove(updatedTask, tasks);
+}
 @*/
 
 
 
 
 
+
 #endif /* VERIFAST_LOCK_PREDICATES_H */