checking bug fix for memory queue, the jury is still out on the formal verification...

diff --git a/Robust/src/Runtime/mlp_runtime.c b/Robust/src/Runtime/mlp_runtime.c
index a9cdb3e0d377a812d20a0297efe9d447b8802d6b..b7a87b559d49465d17953a66ca68629706ee7b73 100644 (file)
--- a/Robust/src/Runtime/mlp_runtime.c
+++ b/Robust/src/Runtime/mlp_runtime.c
@@ -515,7 +515,8 @@ ADDVECTOR(MemoryQueue *Q, REntry *r) {
     flag=(void*)LOCKXCHG((unsigned INTPTR*)&(V->array[index]), (unsigned INTPTR)flag); 
     if (flag!=NULL) {
       if (isParentCoarse(r)) { //parent's retire immediately
-        atomic_dec(&V->item.total);   
+        atomic_dec(&V->item.total);
+        V->index--;
       }
       return READY;
     } else {