please test: Xlib/XCB fixes

[Jamey Sharp]

On Mon, Apr 19, 2010 at 4:49 AM, Simon Thum <simon.thum at gmx.de> wrote:
> I could follow your reasoning and the changes make sense to me. But I
> don't know the overall system enough to pretend that's a review.

It's a good data point, anyway. Thanks!

> Am 19.04.2010 08:33, schrieb Jamey Sharp:
>> Hoping to be Done With Xlib any day now,
>> Jamey
>
> Maybe a good gsoc/student project would be to model Xlib/xcb concurrency
> in e.g. promela, then strike 'Hoping', place 'Confident'. Or similar.

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.

Jamey