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/