From: jjenista <jjenista>
Date: Mon, 16 Aug 2010 21:35:34 +0000 (+0000)
Subject: checking bug fix for memory queue, the jury is still out on the formal verification... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=138ff901fd63232fbcc3f8c2c4a6168bb96234c5;p=IRC.git

checking bug fix for memory queue, the jury is still out on the formal verification of this fix
---

diff --git a/Robust/src/Runtime/mlp_runtime.c b/Robust/src/Runtime/mlp_runtime.c
index a9cdb3e0..b7a87b55 100644
--- 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 {