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