3 ms·

How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for

How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?

oconnore 9y ago
Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
- unboxed_type 9y ago
  Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
  - oconnore 9y ago
    You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended. If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.
    - nickpsecurity 9y ago
      "You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, " This is how I was seeing it happen, too.
    - unboxed_type 9y ago
      Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense. Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.
      - nickpsecurity 9y ago
        No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.
pjmlp 9y ago
A good book about is "Building High Integrity Applications with SPARK". http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/building-high-integrity-applications-spark#YwR5KJ9q84ZfjiLy.97 http://www.cambridge.org/us/academic/subjects/computer-scien... Ada/SPARK has parallel computations defined at language level, known as tasks.
- unboxed_type 9y ago
  Thanks for the reference.

oconnore 9y ago

Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.

unboxed_type 9y ago
Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
- oconnore 9y ago
  You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended. If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.
  - nickpsecurity 9y ago
    "You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, " This is how I was seeing it happen, too.
  - unboxed_type 9y ago
    Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense. Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.
    - nickpsecurity 9y ago
      No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.

pjmlp 9y ago

A good book about is "Building High Integrity Applications with SPARK". http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/building-high-integrity-applications-spark#YwR5KJ9q84ZfjiLy.97 http://www.cambridge.org/us/academic/subjects/computer-scien... Ada/SPARK has parallel computations defined at language level, known as tasks.

unboxed_type 9y ago
Thanks for the reference.