On Mon, Apr 19, 2010 at 4:49 AM, Simon Thum <[email protected]> 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 _______________________________________________ [email protected]: X.Org development Archives: http://lists.x.org/archives/xorg-devel Info: http://lists.x.org/mailman/listinfo/xorg-devel
