please test: Xlib/XCB fixes

[Simon Thum]

Am 19.04.2010 20:26, schrieb Jamey Sharp:
> Yes, I used to know someone who used Promela/Spin, and that would be awesome.
> 
> 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?

--
Simon