The Austin Protocol Compiler

| The Austin Protocol Compiler, the book | News | Source | Documentation | License | APDNS | APC-examples | Authors | SourceForge project |

The Austin Protocol Compiler is a system supporting the development of asyncronous message-passing network protocols, currently focused on protocols based on UDP. The protocol compiler transforms a domain-specific language, the Timed Abstract Protocol notation, to C code and supplies a runtime environment for the Berkeley sockets interface.

The Timed Abstract Protocol notation, or TAP, is a small, simple language designed specifically for describing asynchronous message-passing network protocols with the ultimate goal of verification. TAP is based on the Abstract Protocol notation, or AP, developed by Mohamed G. Gouda, which takes a very abstract, high level approach to network protocols. Unfortunately, AP makes very strong guarantees about time, concurrency, and failure that make protocol verification easy but protocol implementation difficult.

Timed Abstract Protocol notation modifies AP slightly, preserving the ease of verification while adding the ability to express temporal behavior and moving slightly towards implementability. It is based on two execution models: a high-level, abstract model allowing protocols to be understood and verified readily, and a low-level, concrete model which makes efficient implementation possible. The relationship between these two models, which is described in detail later, is complex. However, in short, for many protocols the two models are equivalent---a protocol implemented according to the concrete model behaves the same as a protocol understandable in the abstract model.

The Austin Protocol Compiler, or APC, transforms a process described in TAP into executable code in C. The combination of the Timed Abstract Protocol notation with the Austin Protocol Compiler satisfies the three classes of network protocol development problems in the following ways:

1. The simple domain-specific language of TAP, with its underlying formal model, addresses the intrinsic problems of protocol development through its clarity and verifiability.
2. The clarity of the TAP language, along with the fast turn-around of a compiler, allows practical experience with a protocol while it is still in development.
3. The formal TAP notation, with its emphasis on the protocol's details, and the ability of the compiler to create a running reference model create an environment where the compatibility problems in protocol development can be handled.

In use, the philosophy behind APC is similar to that of yacc---to provide a simple, flexible interface to complex underlying techniques. Within this philosophy, a protocol specification is written in TAP, based on the abstract execution model. APC then translates that specification into an executable system, based on the concrete execution model.

The most important requirement for APC is to correctly implement the concrete execution model of the TAP notation. Some parts of this requirement are necessarily assumptions made about the execution environment and others are implemented by the systems on which APC is based, but the major component of the requirement must be dealt with by the APC implementation. Additionally, there are two further goals for APC:

• Integration with the C systems programming language. TAP, the language provided by APC, is necessarily simple and by design does not contain many features necessary to a general-purpose programming language. Rather than extending this language, APC provides for protocols to call arbitrary C functions, allowing file input/output, cryptography, database and buffer management, and other tasks to be handled in the manner best suited for each of them.
• Simplicity of implementation. Before APC can meet any other goals, its correct operation must be assured. By keeping the implementation simple and the compiler's output understandable, this assurance can be validated.

APC generates portable C code. The file containing the TAP source is filename.ap, the file filename.c contains function definitions, and the file filename.h contains the data structure definitions and function prototypes.

The Austin Protocol Compiler

The Austin Protocol Compiler has been published!

The Austin Protocol Compiler, by Tommy M. McGuire and Mohamed G. Gouda, describes APC and the TAP language and provides the formal background for development of network protocols using them. It also provides example protocols implemented using APC.

Back cover text:

The Austin Protocol Compiler presents a protocol specification language called the Timed Abstract Protocol (TAP) notation. This book will finally close the communication gap between the protocol verifiers and the protocol implementers.

The TAP notation uses two types of semantics: an abstract semantics that appeals to the protocol verifiers and a concrete semantics which appeals to the protocol implementers. The Austin Protocol Compiler illustrates that the two types of semantics of TAP are equivalent. Thus, the correctness of TAP specification of some protocol, that is established based on the abstract semantics of TAP, is maintained when this specification is implemented based on concrete semantics of TAP. The equivalence between the abstract and concrete semantics of TAP suggests the following three-step method for developing a correct implementation of a protocol in this book:

1. Specify the protocol using the TAP notation.
2. Verify the correctness of the specification based on the abstract semantics of TAP.
3. Implement the specification based on the concrete semantics of TAP.

For step 3, this book introduces the Austin Protocol Compiler (APC) that takes as input, a TAP specification of some protocol, and produces as output C-code that implements this protocol based on the concrete semantics of TAP. The Austin Protocol Compiler is designed for a professional audience composed of protocol designers, verifiers, reviewers and implementers. This volume is also suitable for graduate-level students in computer science and electrical engineering.

The ISBN is 0-387-23227-3.

News

• 31 May 2005 : APC-1.2: Building under CYGWIN was broken by the assumption that Python extensions ended in .so; this should be fixed now.

  By the way, I got the first royalty statement for The Austin Protocol Compiler; I would like to personally thank everyone who bought every one of those 72 copies. For everyone else: could you buy, say, six more copies? Springer doesn't send checks for less than $50 unless I ask.

• 20 May 2005 : Initial SourceForge release (very close to) set up.
• 1 Feb 2005 : The Austin Protocol Compiler released. (Or, at least, I got the Author's Copies.)
• 31 July 2004 APC-1.1: APC-1.1 released. Accepts ^M (carriage return) characters as whitespace rather than generating an error.
• 5 May 2004 APC-1.0: APC-1.0 released. This is the first official release with the reference manual and the final version of the algorithm used by the runtime engine.
• 5 May 2004 apc-examples-1.0: apc-examples-1.0 released. Contains the accelerated heartbeat and secret key exchange protocol used as examples in Correct Implementation of Network Protocols.
• 5 May 2004 apdns-1.0: Simple, partial implementation of an authoritative DNS server used as an example in Correct Implementation of Network Protocols.
• 9 Dec 2003 APC-0.5: APC-0.5 released. This version is feature-complete, including support for multiple local processes and local message passing. There have been many changes to both the compiler and runtime library. Once a new version of the reference manual is complete, this version will become the 1.0 release.
• 9 Dec 2003 apdns-0.9: apdns-0.9 released. This is the first publicly-visible version of the DNS server test and example for the APC system.
• 18 Mar 2003 APC-0.4: APC-0.4.tar.gz released. New message size field and boolean type.
• 23 Sep 2002 APC-0.3: APC-0.3.tar.gz released. Improved documentation, better message definition, bug fixes.
• 13 Mar 2002 APC-0.2: APC-0.2.tar.gz released. Uses the new, improved parser toolkit.
• 3 Feb 2002 : New, more complete PostScript and PDF reference manual is available.
• 18 Jan 2002 APC-0.1: APC-0.1.tar.gz released.

Source code

• APC-1.2.tar.gz
• APC-1.1.tar.gz
• APC-1.0.tar.gz
• apc-examples-1.0.tar.gz
• apdns-1.0.tar.gz
• APC-0.5.tar.gz
• apdns-0.9.tar.gz
• APC-0.4.tar.gz
• APC-0.3.tar.gz
• APC-0.2.tar.gz
• APC-0.1.tar.gz

Documentation

• The Austin Protocol Compiler: Tommy M. McGuire and Mohamed G. Gouda. Springer, 2005.
• The Austin Protocol Compiler Reference Manual: Technical Report UTCS-TR02-05, The University of Texas at Austin, 2002. [PDF]
• Correct Implementation of Network Protocols: [PS] [PDF]

License

GNU General Public License, Version 2

APDNS

The apdns package provides simple DNS tools implemented using the Austin Protocol Compiler. The two major components of apdns are:

• aserv, a basic authoritative server. See the aserv(1) man page
• apdns-watcher, a DNS protocol monitor. See the apdns-watcher(1) man page.

apc-examples

This package provides a basic set of test programs and examples for the APC system. They are described in both Correct Implementation of Network Protocols and in The Austin Protocol Compiler.

Authors

• Tommy M. McGuire