More Web Proxy on the site http://driver.im/

research-article

Open access

Kleene algebra modulo theories: a framework for concrete KATs

Authors:

Michael Greenberg,

Eric CampbellAuthors Info & Claims

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 594 - 608

https://doi.org/10.1145/3519939.3523722

Published: 09 June 2022 Publication History

Abstract

Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational theory sound and complete, and coming up with an efficient implementation is still an expert’s task. Abstruse metatheory is holding back KAT’s potential.

We offer a fast path to a “minimum viable model” of a KAT, formally or in code through our framework, Kleene algebra modulo theories (KMT). Given primitives and a notion of state, we can automatically derive a corresponding KAT’s semantics, prove its equational theory sound and complete with respect to a tracing semantics (programs are denoted as traces of states), and derive a normalization-based decision procedure for equivalence checking. Our framework is based on pushback, a generalization of weakest preconditions that specifies how predicates and actions interact. We offer several case studies, showing tracing variants of theories from the literature (bitvectors, NetKAT) along with novel compositional theories (products, temporal logic, and sets). We derive new results over unbounded state, reasoning about monotonically increasing, unbounded natural numbers. Our OCaml implementation closely matches the theory: users define and compose KATs with the module system.

References

[1]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). ACM, New York, NY, USA. 113–126. https://doi.org/10.1145/2535838.2535862

Digital Library

[2]

Allegra Angus and Dexter Kozen. 2001. Kleene Algebra with Tests and Program Schematology. Cornell University, Ithaca, NY, USA. https://doi.org/1813/5831

[3]

Timos Antonopoulos, Eric Koskinen, and Ton Chanh Le. 2019. Specification and inference of trace refinement relations. Proc. ACM Program. Lang., 3, OOPSLA (2019), 178:1–178:30. https://doi.org/10.1145/3360604

Digital Library

[4]

Mina Tahmasbi Arashloo, Yaron Koral, Michael Greenberg, Jennifer Rexford, and David Walker. 2016. SNAP: Stateful Network-Wide Abstractions for Packet Processing. In Proceedings of the 2016 ACM SIGCOMM Conference (SIGCOMM ’16). ACM, New York, NY, USA. 29–43. https://doi.org/10.1145/2934872.2934892

Digital Library

[5]

Jorge A. Baier and Sheila A. McIlraith. 2006. Planning with First-order Temporally Extended Goals Using Heuristic Search. In National Conference on Artificial Intelligence (AAAI’06). AAAI Press, 788–795. isbn:978-1-57735-281-5 http://dl.acm.org/citation.cfm?id=1597538.1597664

[6]

Mike Barnett and K. Rustan M. Leino. 2005. Weakest-precondition of Unstructured Programs. In Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE ’05). ACM, New York, NY, USA. 82–87. https://doi.org/10.1145/1108768.1108813

Digital Library

[7]

Adam Barth and Dexter Kozen. 2002. Equational verification of cache blocking in LU decomposition using Kleene algebra with tests. Cornell University. https://hdl.handle.net/1813/5848

[8]

Ryan Beckett, Michael Greenberg, and David Walker. 2016. Temporal NetKAT. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, New York, NY, USA. 386–401. https://doi.org/10.1145/2908080.2908108

Digital Library

[9]

Eric Campbell and Michael Greenberg. 2021. Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic. CoRR, arXiv:2107.06045.

[10]

Eric Hayden Campbell. 2017. Infiniteness and Linear Temporal Logic: Soundness, Completeness, and Decidability. Pomona College.

[11]

Ernie Cohen. 1994. Hypotheses in Kleene Algebra. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.6067

[12]

Ernie Cohen. 1994. Lazy Caching in Kleene Algebra. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.5074

[13]

Ernie Cohen. 1994. Using Kleene algebra to reason about concurrency control. Telcordia.

[14]

Ernie Cohen and Dexter Kozen. 2000. A note on the complexity of propositional Hoare logic. ACM Trans. Comput. Log., 1, 1 (2000), 171–174. https://doi.org/10.1145/343369.343404

Digital Library

[15]

Anupam Das and Damien Pous. 2017. A Cut-Free Cyclic Proof System for Kleene Algebra. In Automated Reasoning with Analytic Tableaux and Related Methods, Renate A. Schmidt and Cláudia Nalon (Eds.). Springer International Publishing, Cham. 261–277. isbn:978-3-319-66902-1 https://doi.org/10.1007/978-3-319-66902-1_16

[16]

Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. 2014. Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness. In AAAI. 1027–1033. https://www.diag.uniroma1.it/degiacom/papers/2014/AAAI14.pdf

[17]

Giuseppe De Giacomo and Moshe Y Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI’13 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence. 854–860. https://www.ijcai.org/Proceedings/13/Papers/132.pdf

[18]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg. 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

[19]

Leonardo De Moura and Nikolaj Bjørner. 2011. Satisfiability Modulo Theories: Introduction and Applications. Commun. ACM, 54, 9 (2011), Sept., 69–77. https://doi.org/10.1145/1995376.1995394

Digital Library

[20]

Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM, 18, 8 (1975), Aug., 453–457. https://doi.org/10.1145/360933.360975

Digital Library

[21]

Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, and David Walker. 2011. Frenetic: a network programming language. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011. 279–291. https://doi.org/10.1145/2034773.2034812

Digital Library

[22]

Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 282–309. https://doi.org/10.1007/978-3-662-49498-1_12

Digital Library

[23]

Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, New York, NY, USA. 343–355. https://doi.org/10.1145/2676726.2677011

Digital Library

[24]

Carlo A. Furia and Bertrand Meyer. 2009. Inferring Loop Invariants using Postconditions. CoRR, arXiv:0909.0884.

[25]

Carlo Alberto Furia and Bertrand Meyer. 2010. Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday. Springer Berlin Heidelberg, Berlin, Heidelberg. 277–300. isbn:3642150241 https://doi.org/10.1007/978-3-642-15025-8_15

[26]

Murdoch J. Gabbay and Vincenzo Ciancia. 2011. Freshness and Name-restriction in Sets of Traces with Names. In Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures: Part of the Joint European Conferences on Theory and Practice of Software (FOSSACS’11/ETAPS’11). Berlin, Heidelberg. 365–380. https://doi.org/10.1007/978-3-642-19805-2_25

[27]

Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller. 2014. Automating Full Functional Verification of Programs with Loops. CoRR, arXiv:1407.5286.

[28]

Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. 2014. KAT + B!. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS ’14). ACM, New York, NY, USA. Article 44, 44:1–44:10 pages. https://doi.org/10.1145/2603088.2603095

Digital Library

[29]

Arjun Guha, Mark Reitblatt, and Nate Foster. 2013. Machine-verified network controllers. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013. 483–494. https://doi.org/10.1145/2491956.2462178

Digital Library

[30]

Soonho Kong, Yungbum Jung, Cristina David, Bow-Yaw Wang, and Kwangkeun Yi. 2010. Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates. In Proceedings of the 8th Asian Conference on Programming Languages and Systems (APLAS’10). 328–343. https://doi.org/10.1007/978-3-642-17164-2_23

[31]

Dexter Kozen. 1997. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst., 19, 3 (1997), May, 427–443. issn:0164-0925 https://doi.org/10.1145/256167.256195

Digital Library

[32]

Dexter Kozen. 2003. Kleene algebra with tests and the static analysis of programs. Cornell University. https://hdl.handle.net/1813/5627

[33]

Dexter Kozen. 2004. Some results in dynamic model theory. Science of Computer Programming, 51, 1 (2004), 3 – 22. issn:0167-6423 https://doi.org/10.1016/j.scico.2003.09.004 Mathematics of Program Construction (MPC 2002)

Digital Library

[34]

Dexter Kozen. 2017. On the Coalgebraic Theory of Kleene Algebra with Tests. In Rohit Parikh on Logic, Language and Society. Springer, 279–298. https://doi.org/10.1007/978-3-319-47843-2_15

[35]

Dexter Kozen and Konstantinos Mamouras. 2014. Kleene Algebra with Equations. In Automata, Languages, and Programming: 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 280–292. https://doi.org/10.1007/978-3-662-43951-7_24

[36]

Dexter Kozen and Maria-Christina Patron. 2000. Certification of Compiler Optimizations Using Kleene Algebra with Tests. In Proceedings of the First International Conference on Computational Logic (CL ’00). Springer-Verlag, London, UK, UK. 568–582. isbn:3-540-67797-6 https://doi.org/10.1007/3-540-44957-4_38

[37]

Kim G Larsen, Stefan Schmid, and Bingtian Xue. 2016. WNetKAT: Programming and Verifying Weighted Software-Defined Networks. In OPODIS. https://doi.org/10.4230/LIPIcs.OPODIS.2016.18

[38]

Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Černý. 2016. Event-driven Network Programming. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, New York, NY, USA. 369–385. https://doi.org/10.1145/2908080.2908097

Digital Library

[39]

Christopher Monsanto, Nate Foster, Rob Harrison, and David Walker. 2012. A compiler and run-time system for network programming languages. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. 217–230. https://doi.org/10.1145/2103656.2103685

Digital Library

[40]

Yoshiki Nakamura. 2015. Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative. RAMiCS 2015, 1. http://ceur-ws.org/Vol-1454/ramics15-st_1-8.pdf

[41]

Greg Nelson and Derek C. Oppen. 1979. Simplification by Cooperating Decision Procedures. ACM Trans. Program. Lang. Syst., 1, 2 (1979), Oct., 245–257. https://doi.org/10.1145/357073.357079

Digital Library

[42]

Saswat Padhi, Rahul Sharma, and Todd Millstein. 2016. Data-driven Precondition Inference with Learned Features. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). New York, NY, USA. 42–56. https://doi.org/10.1145/2908080.2908099

Digital Library

[43]

Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). New York, NY, USA. 357–368. https://doi.org/10.1145/2676726.2677007

Digital Library

[44]

Mark Reitblatt, Marco Canini, Arjun Guha, and Nate Foster. 2013. FatTire: declarative fault tolerance for software-defined networks. In Proceedings of the Second ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking, HotSDN 2013, The Chinese University of Hong Kong, Hong Kong, China, Friday, August 16, 2013. 109–114. https://doi.org/10.1145/2491185.2491187

Digital Library

[45]

Grigore Roşu. 2016. Finite-Trace Linear Temporal Logic: Coinductive Completeness. In International Conference on Runtime Verification. 333–350. https://doi.org/10.1007/s10703-018-0321-3

Digital Library

[46]

J. J.M.M. Rutten. 1996. Universal Coalgebra: A Theory of Systems. CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, The Netherlands. https://doi.org/10.1016/S0304-3975(00)00056-6

Digital Library

[47]

Andrew E. Santosa. 2015. Comparing Weakest Precondition and Weakest Liberal Precondition. CoRR, arXiv:1512.04013.

[48]

Cole Schlesinger, Michael Greenberg, and David Walker. 2014. Concurrent NetCore: From Policies to Pipelines. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). ACM, New York, NY, USA. 11–24. https://doi.org/10.1145/2692915.2628157

Digital Library

[49]

Rahul Sharma and Alex Aiken. 2014. From Invariant Checking to Invariant Inference Using Randomized Search. In Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559. New York, NY, USA. 88–105. https://doi.org/10.1007/s10703-016-0248-5

Digital Library

[50]

Alexandra Silva. 2010. Kleene Coalgebra. University of Minho. Braga, Portugal. https://alexandrasilva.org/files/thesis.pdf

[51]

Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha. 2015. A Fast Compiler for NetKAT. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). ACM, New York, NY, USA. 328–341. https://doi.org/10.1145/2784731.2784761

Digital Library

[52]

Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. 2020. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang., 4, POPL (2020), 61:1–61:28. https://doi.org/10.1145/3371129

Digital Library

[53]

Aaron Stump, Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. 2001. A Decision Procedure for an Extensional Theory of Arrays. In LICS. https://doi.org/10.1109/LICS.2001.932480

Cited By

Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Chen QBanerjee ADemiralp ÇDurrett GDillig I(2023)Data Extraction via Semantic Regular Expression SynthesisProceedings of the ACM on Programming Languages10.1145/36228637:OOPSLA2(1848-1877)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622863
Antonopoulos TKoskinen ELe TNagasamudram RNaumann DNgo M(2023)An Algebra of Alignment for Relational VerificationProceedings of the ACM on Programming Languages10.1145/35712137:POPL(573-603)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571213
Show More Cited By

Index Terms

Kleene algebra modulo theories: a framework for concrete KATs
1. Software and its engineering
2. Theory of computation
  1. Formal languages and automata theory
    1. Regular languages

Recommendations

Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time

Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show ...
Representability of Kleene Posets and Kleene Lattices
Abstract
A Kleene lattice is a distributive lattice equipped with an antitone involution and satisfying the so-called normality condition. These lattices were introduced by J. A. Kalman. We extended this concept also for posets with an antitone involution. ...
On Hoare Logic and Kleene Algebra with Tests
LICS '99: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science

We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary equational reasoning. It follows from the reduction that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2022

1038 pages

ISBN:9781450392655

DOI:10.1145/3519939

General Chair:
Ranjit Jhala
University of California at San Diego, USA
,
Program Chair:
Işil Dillig
University of Texas at Austin, USA

Copyright © 2022 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '22

Sponsor:

SIGPLAN

PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 13 - 17, 2022

CA, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
469
Total Downloads

Downloads (Last 12 months)164
Downloads (Last 6 weeks)11

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Chen QBanerjee ADemiralp ÇDurrett GDillig I(2023)Data Extraction via Semantic Regular Expression SynthesisProceedings of the ACM on Programming Languages10.1145/36228637:OOPSLA2(1848-1877)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622863
Antonopoulos TKoskinen ELe TNagasamudram RNaumann DNgo M(2023)An Algebra of Alignment for Relational VerificationProceedings of the ACM on Programming Languages10.1145/35712137:POPL(573-603)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571213
Kappé TSchmid TSilva A(2023)A Complete Inference System for Skip-free Guarded Kleene Algebra with TestsProgramming Languages and Systems10.1007/978-3-031-30044-8_12(309-336)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_12

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents