please test: Xlib/XCB fixes

[Jamey Sharp]

On Wed, Apr 21, 2010 at 10:11 AM, Simon Thum <simon.thum at gmx.de> wrote:
> Am 19.04.2010 20:26, schrieb Jamey Sharp:
>> We actually have proofs or proof sketches for parts of XCB, so for
>> example I am Confident that pure XCB applications will never fail to
>> insert GetInputFocus requests when needed to maintain sequence number
>> synchronization, and also that it will always do so at the last
>> possible instant. (I can also prove by counterexample that Xlib
>> doesn't have either of these properties :-/ which would require huge
>> ABI changes to fix.) We haven't used model-checkers for that, just
>> logic and Hoare triples or Z.
>
> Nice! Is that published/documented somewhere?

This thread has reminded me that I never got around to writing up the
proof, so I have a draft in-progress now.

A different proof about XCB is published in "X meets Z"
(http://xcb.freedesktop.org/Publications/), which I'd recommend to
anyone unfamiliar with lightweight formal methods as a good
introduction. Unfortunately XCB doesn't actually use quite the
algorithm it describes, and last time I looked I had some concern
about whether the proof was correct. :-/ But it does correctly explain
one of the problems we encountered that was so hard that we wanted a
proof about it.

Jamey