-
Petr4: Formal Foundations for P4 Data Planes
Authors:
Ryan Doenges,
Mina Tahmasbi Arashloo,
Santiago Bautista,
Alexander Chang,
Newton Ni,
Samwise Parkinson,
Rudy Peterson,
Alaia Solko-Breslin,
Amanda Xu,
Nate Foster
Abstract:
P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-…
▽ More
P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code. Clearly neither of these artifacts is suitable for formal reasoning.
This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a calculus that models the semantics of a core fragment of P4. Throughout the specification, some aspects of program behavior are left up to targets. Our interpreter is parameterized over a target interface which collects all the target-specific behavior in the specification in a single interface.
The specification makes ad-hoc restrictions on the nesting of certain program constructs in order to simplify compilation and avoid the possibility of nonterminating programs. We captured the latter intention in our core calculus by stratifying its type system, rather than imposing unnatural syntactic restrictions, and we proved that all programs in this core calculus terminate.
We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We established termination for the core calculus by induction on the stratified type system. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.
△ Less
Submitted 11 November, 2020;
originally announced November 2020.
-
Sectional-hyperbolic lyapunov stable sets
Authors:
Serafin Bautista,
Yeison Sánchez
Abstract:
In hyperbolic dynamics, a well-known result is: every hyperbolic Lyapunov stable set, is attracting; it's natural to wonder if this result is maintained in the sectional-hyperbolic dynamics. This question is still open, although some partial results have been presented. We will prove that all sectional-hyperbolic transitive Lyapunov stable set of codimension one of a vector field X over a compact…
▽ More
In hyperbolic dynamics, a well-known result is: every hyperbolic Lyapunov stable set, is attracting; it's natural to wonder if this result is maintained in the sectional-hyperbolic dynamics. This question is still open, although some partial results have been presented. We will prove that all sectional-hyperbolic transitive Lyapunov stable set of codimension one of a vector field X over a compact manifold, with unique singularity Lorenz-like, which is of boundary-type, is an attractor of X.
△ Less
Submitted 2 April, 2018;
originally announced April 2018.
-
Sectional connecting lemma
Authors:
Serafin Bautista,
Valdiane Sales,
Yeison Sánchez
Abstract:
A hyperbolic set on a compact manifold M, satisfies the property: given two of your any points p and q, such that for all positive ε>0, there is a trajectory in the hyperbolic set from a point ε-close to p to a point ε-close to q, then there is a point in M whose α-limit is that of p and whose ω-limit is that of q. Bautista and Morales give a version of this property, for sectional-Anosov flows (v…
▽ More
A hyperbolic set on a compact manifold M, satisfies the property: given two of your any points p and q, such that for all positive ε>0, there is a trajectory in the hyperbolic set from a point ε-close to p to a point ε-close to q, then there is a point in M whose α-limit is that of p and whose ω-limit is that of q. Bautista and Morales give a version of this property, for sectional-Anosov flows (vector fields whose maximal invariant set is sectional-hyperbolic), including some conditions; among them that limit the dimension of M to three. In this paper, we prove a generalization of this result, for sectional-hyperbolic sets of codimension one in high dimensions.
△ Less
Submitted 2 April, 2018;
originally announced April 2018.
-
Intransitive sectional-Anosov flows on 3-manifolds
Authors:
S. Bautista,
A. M. López,
H. M. Sánchez
Abstract:
For each $n\in\mathbb{Z}^+$, we show the existence of Venice masks (i.e. intransitive sectional-Anosov flows with dense periodic orbits) containing $n$ equilibria on certain compact 3-manifolds. These examples are characterized because of the maximal invariant set is a finite union of homoclinic classes. Here, the intersection between two different homoclinic classes is contained in the closure of…
▽ More
For each $n\in\mathbb{Z}^+$, we show the existence of Venice masks (i.e. intransitive sectional-Anosov flows with dense periodic orbits) containing $n$ equilibria on certain compact 3-manifolds. These examples are characterized because of the maximal invariant set is a finite union of homoclinic classes. Here, the intersection between two different homoclinic classes is contained in the closure of the union of unstable manifolds of the singularities.
△ Less
Submitted 26 November, 2017;
originally announced November 2017.
-
On the intersection of sectional-hyperbolic sets
Authors:
S. Bautista,
C. A. Morales
Abstract:
We analyse the intersection of positively and negatively sectional-hyperbolic sets for flows on compact manifolds. First we prove that such an intersection is hyperbolic if the intersecting sets are both transitive (this is false without such a hypothesis). Next we prove that, in general, such an intersection consists of a nonsingular hyperbolic set, finitely many singularities and regular orbits…
▽ More
We analyse the intersection of positively and negatively sectional-hyperbolic sets for flows on compact manifolds. First we prove that such an intersection is hyperbolic if the intersecting sets are both transitive (this is false without such a hypothesis). Next we prove that, in general, such an intersection consists of a nonsingular hyperbolic set, finitely many singularities and regular orbits joining them. Afterward we exhibit a three-dimensional star flow with two homoclinic classes, one being positively (but not negatively) sectional-hyperbolic and the other negatively (but not positively) sectional-hyperbolic, whose intersection reduces to a single periodic orbit. This provides a counterexample to a conjecture by Shy, Zhu, Gan and Wen (\cite{sgw}, \cite{zgw}).
△ Less
Submitted 2 October, 2014;
originally announced October 2014.
-
On the essential hyperbolicity of sectional-Anosov flows
Authors:
S. Bautista,
C. A. Morales
Abstract:
We prove that every sectional-Anosov flow of a compact 3-manifold $M$ exhibits a finite collection of hyperbolic attractors and singularities whose basins form a dense subset of $M$. Applications to the dynamics of sectional-Anosov flows on compact 3-manifolds include a characterization of essential hyperbolicity, sensitivity to the initial conditions (improving \cite{ams}) and a relationship betw…
▽ More
We prove that every sectional-Anosov flow of a compact 3-manifold $M$ exhibits a finite collection of hyperbolic attractors and singularities whose basins form a dense subset of $M$. Applications to the dynamics of sectional-Anosov flows on compact 3-manifolds include a characterization of essential hyperbolicity, sensitivity to the initial conditions (improving \cite{ams}) and a relationship between the topology of the ambient manifold and the denseness of the basin of the singularities.
△ Less
Submitted 13 June, 2013;
originally announced June 2013.
-
Topological gravity on plumbed V-cobordisms
Authors:
Vladimir N. Efremov,
Nikolai V. Mitskievich,
Alfonso M. Hernandez Magdaleno,
Ramona Serrano Bautista
Abstract:
An ensemble of cosmological models based on generalized BF-theory is constructed where the role of vacuum (zero-level) coupling constants is played by topologically invariant rational intersection forms (cosmological-constant matrices) of 4-dimensional plumbed V-cobordisms which are interpreted as Euclidean spacetime regions. For these regions describing topology changes, the rational and intege…
▽ More
An ensemble of cosmological models based on generalized BF-theory is constructed where the role of vacuum (zero-level) coupling constants is played by topologically invariant rational intersection forms (cosmological-constant matrices) of 4-dimensional plumbed V-cobordisms which are interpreted as Euclidean spacetime regions. For these regions describing topology changes, the rational and integer intersection matrices are calculated. A relation is found between the hierarchy of certain elements of these matrices and the hierarchy of coupling constants of the universal (low-energy) interactions.
PACS numbers: 0420G, 0240, 0460
△ Less
Submitted 11 February, 2005; v1 submitted 11 February, 2005;
originally announced February 2005.
