From e4db1f8aba02c24a814e4d26d46913bc94a78e67 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Sat, 3 Dec 2022 08:58:19 -0500
Subject: [PATCH] Refined lock invariant to only give read permission to all
 tasks and write permission to locally scheduled task

---
 tasks.c                                          | 16 +++++++++++-----
 verification/verifast/proof/task_predicates.h    |  4 ++++
 .../verifast/proof/verifast_lock_predicates.h    | 11 +++++++----
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/tasks.c b/tasks.c
index 8e36989db..067c66460 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1051,7 +1051,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         mem(pxTaskItem, gCells) == true &*&
                         xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
                         gSize > 0 &*&
-                        foreach(gTasks, sharedSeg_TCB_p) &*&
+                        // Read permissions for every task
+                            foreach(gTasks, readOnly_sharedSeg_TCB_p) 
+                        &*&
+                        // Write permission for task scheduled on this core
+                            [1/2]sharedSeg_TCB_p(gCurrentTCB) 
+                        &*&
                         subset(gOwners, gTasks) == true;
 
                  @*/
@@ -1129,7 +1134,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             #endif
                         #endif
                         {
-                            //@ assert( foreach(remove(pxTCB, gTasks), sharedSeg_TCB_p) );
+                            //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p) );
                             //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] );
                             /*@
                             if( gCurrentTCB == pxTCB ) {
@@ -1138,7 +1143,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             } else {
                                 neq_mem_remove(gCurrentTCB, pxTCB, gTasks);
                                 foreach_remove(gCurrentTCB, remove(pxTCB, gTasks));
-                                open sharedSeg_TCB_p(gCurrentTCB);
                             }
                             @*/
                             /* If the task is not being executed by any core swap it in */
@@ -1157,13 +1161,14 @@ static void prvYieldForTask( TCB_t * pxTCB,
                                 // => We don't have to close anything.
                             } else {
                                 close sharedSeg_TCB_p(gCurrentTCB);
+                                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), sharedSeg_TCB_p) );
+                            //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p) );
                         }
                     }
                     else if( pxTCB == pxCurrentTCBs[ xCoreID ] )
@@ -1195,7 +1200,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         break;
                     }
 
-                    //@ close sharedSeg_TCB_p(pxTCB);   
+                    //@ close sharedSeg_TCB_p(pxTCB);  
+                    //@ close readOnly_sharedSeg_TCB(pxTCB); 
                     //@ foreach_unremove(pxTCB, gTasks);
                 } while( pxTaskItem != pxLastTaskItem );
 
diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index be610c3d8..ee17bad1f 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -111,6 +111,10 @@ predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) =
 predicate sharedSeg_TCB_p(TCB_t* tcb;) =
     tcb->xTaskRunState |-> ?gTaskRunState;
 
+// Auxiliary predicate to allow foreach-quantification about fraction
+predicate readOnly_sharedSeg_TCB_p(TCB_t* tcb;) =
+    [1/2]sharedSeg_TCB_p(tcb);
+
 predicate coreLocalSeg_TCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) =
     tcb->uxCriticalNesting |-> uxCriticalNesting;
 @*/
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index e473e4eb3..88017fa40 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -97,10 +97,13 @@ predicate taskISRLockInv_p() =
     // tasks / TCBs
         exists_in_taskISRLockInv_p(?gTasks)
         &*&
-        // Access permissions for every task
-        // TODO: Convert to read permissions
-        // ∀t ∈ gTasks. sharedSeg_TCB_p(t)
-            foreach(gTasks, sharedSeg_TCB_p)
+        // (RP-All) Read permissions for every task
+        // ∀t ∈ gTasks. [1/2]sharedSeg_TCB_p(t)
+            foreach(gTasks, readOnly_sharedSeg_TCB_p)
+        &*&
+        // (RP-Current) Read permission for task currently scheduled on this core
+        // (RP-All) + (RP-Current) => Write permission for scheduled task
+            [1/2]sharedSeg_TCB_p(gCurrentTCB)
         &*&
         readyLists_p(?gCellLists, ?gOwnerLists) 
         &*&