Frequently Asked Questions (FAQ)

  1. I’d like to learn how to specify and prove theorems in Prosa. Where should I start?

  2. Your definition of X looks too complicated. You should have used this alternative definition…

  3. Do you claim that, after Prosa, there is no more need for proofs in papers? Aren’t pen-and-paper proofs still important?

  4. Despite Prosa’s focus on readability, the specification and proofs are still far from being accessible to a general audience. In the current state, it can only be used by researchers.

  5. I don’t understand the intuition behind the response-time analyses presented in the Prosa paper.

  6. Why do you have to import ssreflect? Is it really needed in the development?

  7. In the introduction of the Prosa paper, you mention several flaws in the real-time systems literature, yet you do not show how these problems can be fixed. What are the actual limitations of Prosa?

Questions and Answers

  1. I’d like to learn how to specify and prove theorems in Prosa. Where should I start?

    Please have a look at the getting started guide and get in touch.

  2. Your definition of X looks too complicated. You should have used this alternative definition…

    Although we write the specifications with readability in mind, there are still some factors that might cause definitions to seem slightly strange on first sight:

    A combination of these factors may affect how we chose to formalize certain aspects of the formalization. Nevertheless, we don’t claim that our approach is “the only” or “the best way” to formalize real-time scheduling; we always welcome suggestions and discussions. If you have ideas for how to improve the specification and would like to contribute to Prosa, please contact us using the mailing list.

  3. Do you claim that, after Prosa, there is no more need for proofs in papers? Aren’t pen-and-paper proofs still important?

    We by no means argue that pen-and-paper proofs should be subsumed by mechanized proofs; the former are still useful as a teaching tool and will likely remain the de facto standard way of presenting research results.

    What Prosa advocates is a new methodology for verifying the correctness of theorems with the highest degree of confidence, in particular those that are challenging and error-prone. It does not, however, mandate how research should be presented. That should be driven exclusively by the interests of the authors and the scientific community.

    As an example, some researchers in the fields of Programming Languages and Verification continue to provide pen-and-paper proofs or proof sketches in their papers, while still providing mechanized proofs as supplementary material. Although more costly in the short term, this strategy aggregates the benefits of the two approaches and provides many benefits in the long term.

  4. Despite Prosa’s focus on readability, the specification and proofs are still far from being accessible to a general audience. In the current state, it can only be used by researchers.

    Prosa specifically targets researchers in the development of provably-correct schedulability analyses. Real-time systems engineers and other practicioners, instead, indirectly benefit from the artifacts of this research. In particular, tool providers can implement analyses that are guaranteed to be correct, and can also test their implementations against provably correct reference models in Prosa. As a result, end users will eventually benefit from better tools and safer systems.

  5. I don’t understand the intuition behind the response-time analyses presented in the Prosa paper.

    The focus of the ECRTS 2016 Prosa paper is not to discuss particular schedulability results, but to present the proof framework and how it can be applied to different real-time scheduling problems.

    The response-time analyses discussed in the paper stem from Bertogna and Cirinei’s RTA as presented in Chapter 17 of the book Multiprocessor Scheduling for Real-Time Systems by Baruah et al., which differs a bit from the conference version. Please check the book if you would like to understand the formulas, and contact us in case of further questions.

  6. Why do you have to import ssreflect? Is it really needed in the development?

    While third-party proof libraries can admittedly lead to steeper learning curves, ssreflect provides a lot of useful mechanisms for proof management and most of the mathematical foundations required by Prosa, in particular the LaTeX-like operators from bigop, which greatly help with readability.

    Another advantage of ssreflect is that most of the definitions use booleans and can be transparently used in computations (as we do when implementing schedulers). Moreover, since ssreflect has been used in many mathematical proofs, we rarely have to prove foundational lemmas unrelated to real-time scheduling.

    The major difficulty is ssreflect’s scarce documentation: finding the right lemmas from ssreflect is not an easy task, but looking through the existing proofs in Prosa can serve as a good starting point.

  7. In the introduction of the Prosa paper, you mention several flaws in the real-time systems literature, yet you do not show how these problems can be fixed. What are the actual limitations of Prosa?

    Correcting all the papers in the literature is a huge step, even if done with manual proofs, so we believe that a complete transition towards mechanized proofs would demand effort of several research groups and many years of work. But it is definitely feasible in principle.

    In fact, to the best of our knowledge, there are no (practical) limitations on what Prosa can specify (in the context of real-time scheduling theory). Coq has a powerful logic with support for computation (i.e., we can write algorithms with loops and branches), and so far we have not encountered any real-time scheduling concepts that we were not able to specify.

    Difficulties arise, of course, depending on the complexity of the algorithm we need to specify. However, implementing a C compiler or a complete file system is much more challenging than programming a response-time analysis loop. Since prior work has used Coq to successfully carry out these tasks, we are confident that likely all practically relevant real-time schedulability analyses can be formalized in Prosa/Coq.