Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern in normal form is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. The number of structural components can be reduced by unification and anti-unification. Algorithms for both processes have already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language, while generalizing the unification problem and mechanizing a proven-sound solution in Coq, as well as exploring certain possible extensions of the unification algorithm in a semi-formalized manner.

Matching logic is a general formal framework for reasoning about a wide range of theories, with particular emphasis on programming language semantics. Semantic reasoning, such as proof of satisfaction, requires the logic to be expressed within a foundational theory; adopting a dependently typed setting enables well-sortedness in the object theory to correspond directly to well-typedness in the host theory. In this paper, we present the first dependently typed, locally nameless definition of matching μ -logic, including both syntax and semantics, ensuring well-sortedness and local closedness via sorted contexts encoded in type indices. As a result, ill-sorted syntax is unrepresentable, and the semantics of well-sorted elements are guaranteed to lie within the domains of their associated sorts. We also demonstrate how this encoding facilitates model-theoretic reasoning about the consistency of matching logic theories.

We aim to reason about the correctness of behaviour-preserving transformations of Erlang programs. Behaviour preservation is characterised by semantic equivalence. Based upon our existing formal semantics for Core Erlang, we investigate potential definitions of suitable equivalence relations. In particular we adapt a number of existing approaches of expression equivalence to a simple functional programming language that carries the main features of sequential Core Erlang; we then examine the properties of the equivalence relations and formally establish connections between them. The results presented in this paper, including all theorems and their proofs, have been machine checked using the Coq proof assistant.

Target-independent packet processing languages support diverse hardware and software targets by generalizing over the set of primitive operations (extern-functions)available on the target. In P4, the language specification does not specify whether the invocation of an extern function is synchronous or asynchronous - supposedly synchronous by default. However, in some use cases, it makes more sense to invoke such functions in an asynchronous way and let the thread keep processing packets while the extern operation is being performed by a dedicated resource or accelerator device. In this paper, we propose a method for transparent description and efficient implementation of asynchronous extern function calls in P4-programmable software data planes. Our DPDK - based early prototype relies on the concept of coroutines used for saving packet contexts and manual switching between them. The overhead of the proposed solution is analyzed with a packet encryption case study.

Although the programmability of control planes has been thoroughly examined in the past years, only a limited number of studies go beyond the consideration that the data plane is only a collection of simple packet forwarding devices. Even OpenFlow, a popular, very expressive data plane programming language, is still restricted to supporting a subset of existing protocol headers. To overcome such limitations, new data plane programming models have recently emerged. One of the them is P4, a high-level language for programming packet processors that enables great flexibility in the description of packet structures and processing pipelines. In this paper, we propose T4P4S1, a multi-target compiler generating high performance switch programs from P4 descriptions. To support multiple targets, a networking hardware abstraction layer (NetHAL) is defined; the compiler generates a core switch code which is then linked with a target-specific NetHAL implementation. To avoid performance degradation, the boundaries of this separation should be chosen carefully, since the core program is only responsible for target-independent optimization, while the implementation of NetHAL should cover target-dependent enhancements. To analyze the performance, thorough measurements have been carried out, showing that the switch generated by T4P4S can easily scale beyond 100 Gbps.

P4 is a high level language for programming network switches that allows for great flexibility in the description of packet structure and processing, independent of the specifics of the underlying hardware. In this demo, we present our prototype P4 compiler in which the hardware independent and hardware specific functionalities are separated. We have identified the requisites of the latter, which form the interface of our target specific Hardware Abstraction Library (HAL); the compiler turns P4 code into a target independent core program that is linked to this library and invokes its operations. The two stage separation improves portability: to support a new architecture, only the hardware dependent library has to be implemented. In the demo, we demonstrate the flexibility of our compiler with a HAL for Intel DPDK, and show the packet processing and forwarding performance of compiled switches in different scenarios.