Formalizations and algorithms for optimized parallel protocol implementation

We propose a formalized method that allows to au-tomatically derive an optimized implementation from the formal specication of a protocol. Our method starts with the SDL specication of a protocol stack. We rst derive a data and control ow dependence graph from each SDL process. Then, in order to per-form cross-layer optimizations we combine the depen-dence graphs of dierent SDL processes. Next, we de-termine the common path through the multi-layer de-pendence graph. We then parallelize this graph wher-ever possible which yields a relaxed dependence graph. Based on this relaxed dependence graph we interpret dierent optimization concepts that have been sug-gested in the literature, in particular lazy messages and combination of data manipulation operations. To-gether with these interpretations the relaxed depen-dence graph can be be used as a foundation for a compile-time schedule on a sequential or parallel ma-chine architecture. The formalization we provide al-lows our method to be embedded in a more compre-hensive protocol engineering methodology.