From fbf4ba981fae37b99799c11d9e6c08aed460dd30 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Sun, 4 Dec 2022 10:19:48 -0500
Subject: [PATCH] Added lemmas to update read permissions for unscheduled tasks
 after new task has been started.

---
 tasks.c                                       |  3 +
 .../verifast/proof/verifast_lock_predicates.h | 63 +++++++++++++++++++
 2 files changed, 66 insertions(+)

diff --git a/tasks.c b/tasks.c
index 7a2747011..0f9f37b01 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1203,6 +1203,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             /*@ close_updated_foreach_readOnly_sharedSeg_TCB(pxTCB, gTasks, gStates1,
                                                                              gStates2, xCoreID);
                              @*/
+                            /*@ startUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running
+                                    (pxTCB, gTasks, gStates1, gStates2, xCoreID);
+                             @*/
                             //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) );
                             //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) );
 
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index a71eb59f5..f369d7912 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -335,8 +335,71 @@ ensures
             close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2));
     }
 }
+
+lemma void updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running
+            (TCB_t* updatedTask, list<void*> tasks, list<void*> subTasks,
+             list<TaskRunning_t> states, list<TaskRunning_t> updatedStates,
+             TaskRunning_t s)
+requires 
+    distinct(tasks) == true &*&
+    distinct(subTasks) == true &*&
+    length(tasks) == length(states) &*&
+    mem(updatedTask, tasks) == true &*&
+    mem(updatedTask, subTasks) == false &*&
+    subset(subTasks, tasks) == true &*&
+    foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*&
+    updatedStates == update(index_of(updatedTask, tasks), s, states);
+ensures 
+    foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates));
+{
+    switch(subTasks) {
+        case nil:
+            open  foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states));
+            close foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates));
+        case cons(h, t):
+            open foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states));
+
+            // Prove that update preserves state of `h`.
+            index_of_different(h, updatedTask, tasks);
+            nth_update(index_of(h, tasks), index_of(updatedTask, tasks), s, states);
+            assert( nth(index_of(h, tasks), states) == nth(index_of(h, tasks), updatedStates) );
+
+            open readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)(h);
+            close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)(h);
+            updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running
+                (updatedTask, tasks, t, states, updatedStates, s);
+            close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates));
+    }
+}
+
+lemma void startUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running
+            (TCB_t* startedTask, list<void*> tasks,
+             list<TaskRunning_t> states, list<TaskRunning_t> updatedStates,
+             int coreID)
+requires 
+    distinct(tasks) == true &*&
+    length(tasks) == length(states) &*&
+    mem(startedTask, tasks) == true &*&
+    foreach(remove(startedTask, tasks), readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*&
+    updatedStates == update(index_of(startedTask, tasks), coreID, states) &*&
+    0 <= coreID &*& coreID < configNUM_CORES;
+ensures 
+    foreach(tasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates));
+{
+    distinct_remove(startedTask, tasks);
+    distinct_mem_remove(startedTask, tasks);
+    remove_result_subset(startedTask, tasks);
+    updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running
+        (startedTask, tasks, remove(startedTask, tasks), states, updatedStates, 
+         coreID);
+                             
+    assert( foreach(remove(startedTask, tasks), readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)) );
+    close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)(startedTask);
+    foreach_unremove(startedTask, tasks);
+}
 @*/
 
+
 /*@
 lemma list<TaskRunning_t> def_state1(list<void*> tasks,
                                      list<TaskRunning_t> states,