Protocol Switching

Networking properties such as total order or recovery from message loss can be realized by many different protocols. These protocols offer the same functionality but are optimized for different environments or applications. Hybrid protocols can be used to combine the advantages of various protocols, but designing them correctly is difficult. The ENSEMBLE system [#!RBHVK98!#,#!phd:Hayden98a!#] provides a mechanism for switching between different protocols at run-time. So far, however, it was not clear how to guarantee that the result was actually correct, i.e. under what circumstances a switch would actually preserve the properties of the individual protocols. Our new approach to switching is to design a generic switching protocol ($SP$) that would serve as a wrapper for a set of protocols with the same functionality. This switching protocol shall interact with the application in a transparent fashion, that is, the application cannot tell easily that it is running on the $SP$ rather than on one of the underlying protocols, even as the $SP$ switches between protocols. The kinds of uses we envision include the following:

• Performance. By using the best protocol for a particular network and application behavior, performance can always be optimal.
• On-line Upgrading. Protocol switching can be used to upgrade network protocols or fix minor bugs at run-time without having to restart applications.
• Security. System managers will be able to increase security at run-time, for example when an intrusion detection system notices unusual behavior.

In a protocol stacking architecture like the one used in ENSEMBLE the switching protocol will reside on top of the individual protocols, coupled by a multiplexer below them, as illustrated in the following diagram. ? --------------------------------------? ??

? --------------------------------------? The basic idea of the switching protocol is to operate in one of two modes. In normal mode it simply forwards messages from the application to the current protocol and vice versa. When there is a request to switch to a different protocol, the $SP$ goes into switching mode, during which any process will deliver all messages for the previous protocol while buffering messages that are to be delivered for the new one. The $SP$ will return to normal mode as soon as all messages for the previous protocol have been delivered. ? ------------------------------?

? ------------------------------? The above description served as the starting point for proving the correctness of the resulting hybrid protocol and subsequently for the implementation of the switching protocol as well. Our verification proceeds in two phases. We first classify communication properties that are switchable, i.e. have the potential to be preserved under switching, and then derive a switching invariant that a switching protocol must satisfy to preserve switchable properties.