Messages in this thread | | | From | "Peter T. Breuer" <> | Subject | Re: spin_unlock optimization(i386) | Date | Fri, 26 Nov 1999 23:38:12 +0100 (MET) |
| |
"Ingo Molnar wrote:" > > the correct one is: > > CPU0 CPU1 > > for (;;) { for (;;) { > i++; b = j; > j++; a = i; > } if (a < b) > BUG(); > }
Just to confirm what you are saying:
invariant: j <= i <= j+1 invariant: b <= a
and this test can indeed never be activated. But ...
> the 'symmetric' test: > > CPU0 CPU1 > > for (;;) { for (;;) { > i1++; i2++; > j1++; j2++; > b = j2; b = j1; > a = i2; a = i1; > if (a < b) if (a < b) > BUG(); BUG(); > } }
invariant: j1 <= i1 <= j1+1 invariant: j2 <= i2 <= j2+1
But that's all! You can get
i1= 50 i2= 100 j1= 50 j2= 100 . b = 50 b = 100 . . a = 50 . TEST a = 100 .
which then tests with a < b on the right. I think ... (this gets confusing).
Peter
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/
| |