Check out the new USENIX Web site.

Home About USENIX Events Membership Publications Students
2002 FREENIX Track Technical Program - Abstract

X Meets Z: Verifying Correctness In
The Presence Of POSIX Threads

Bart Massey, Computer Science Department, Portland State University; Robert Bauer, Rational Software Corporation


The engineering of freely-available UNIX software normally utilizes an informal analysis and design process coupled with extensive user testing. While this approach is often appropriate, there are situations for which it produces less-than-stellar results.

A case study is given of such a situation that arose during the design and implementation of a thread-safe library for interaction with the X Window System. XCB is a C binding library for the X protocol designed to work transparently with either single-threaded or multi-threaded clients. Managing XCB client thread access to the X server while honoring the constraints of both XCB and the X server is thus a delicate matter.

The problem of ensuring that this complex system is coded correctly can be attacked through the use of lightweight formal methods. A model is constructed of the troublesome portion of the system using the Z formal specification notation. This model is used to establish important system properties and produce C code with a high likelihood of correctness.

  • View the full text of this paper in HTML and PDF.
    The Proceedings are published as a collective work, © 2002 by the USENIX Association. All Rights Reserved. Rights to individual papers remain with the author or the author's employer. Permission is granted for the noncommercial reproduction of the complete work for educational or research purposes. USENIX acknowledges all trademarks within this paper.

  • If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.

  • To become a USENIX Member, please see our Membership Information.
?Need help? Use our Contacts page.

Last changed: 16 May 2002 ml
Technical Program
Conference index