HackerPapers

arXiv:1710.07047cs.PL

Safe Pointers in SPARK 2014

Georges-Axel Jaloyan

Abstract

In the context of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-defined subset of the Ada language, intended for formal verification of mission-critical software. Our solution is based on static alias analysis inspired by Rust's borrow-checker and affine types, and enforces the Concurrent Read, Exclusive Write principle. This analysis has been implemented in the GNAT Ada compiler and tested against a number of challenging examples including parts of real-life applications. Our tests show that only minor changes in the source code are required to fit the idiomatic Ada code into SPARK extended with pointers, which is a significant improvement upon the previous state of the art. The proposed extension has been approved by the Language Design Committee for SPARK for inclusion in a future version of SPARK, and is being discussed by the Ada Rapporteur Group for inclusion in the next version of Ada. In the report, we give a formal presentation of the analysis rules for a miniature version of SPARK and prove their soundness. We discuss the implementation and the case studies, and compare our solution with Rust.

arXiv comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 3 identifiable commenters in 5 comments across 5 threads, from Dec 2017 to May 2021. Found in 1 HN submission from Dec 2017 to Dec 2017. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments5 threads

  1. An intro to Zig's integer casting for C programmers 1 comment

    • It can employ, but you do not have to (you can turn off all runtime checks and use formal verification only, something that Rust cannot do (statically verify correctness the same way you can with SPARK using GNATprove)), it can all be done at compile-time with Ada/SPARK. > These…

      johnisgoodView on HNParent context

  2. Ask HN: C with a Borrow-Checker 1 comment

    • Probably SPARK (programming language derived from Ada with advanced proof capabilities). The next release of SPARK will support pointer ownership similar to the Rust borrow checker: https://blog.adacore.com/using-pointers-in-spark https://arxiv.org/pdf/1710.07047.pdf Concurrency…

      thesuperbigfrogView on HNParent context

  3. Why Ada Is the Language You Want to Be Programming Your Systems With 1 comment

    • I would recommend https://www.adacore.com/uploads/books/pdf/ePDF-Implementatio... for more information regarding contracts. There are of course a LOT more, just fire up your preferred search engine and enjoy your findings. :) > SPARK builds on the strengths of Ada to provide…

      johnisgoodView on HNParent context

  4. Rust: Beyond the Typechecker 1 comment

    • Nice! I did not have a chance to look at the issue discussion. Thank you for pointing it out. It's good to see that Rust is learning from Ada. Ada is also learning from Rust: https://arxiv.org/abs/1710.07047

      thesuperbigfrogView on HNParent context

  5. Red Lang goes blockchain 1 comment

    • “but after studying many other ICO, I am convinced now that this is not just a short-lived fad, but a real new model to fund projects, and especially open-source projects related to blockchains.” There’s been quite a few of us suggesting people jump into blockchain just to get…

      nickpsecurityView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.