[Haskell-cafe] Informal modelling and simulation of protocols

[Ivan Perez]

On Sun, 10 Mar 2019 at 20:20, P Orrifolius <porrifolius at gmail.com> wrote:

> On Wed, 6 Mar 2019 at 02:30, Ivan Perez <ivanperezdominguez at gmail.com>
> wrote:
> >
> > Hi
> >
> > Partly related; for recent work we did two things:
> >
> > - Model part of the collision avoidance logic of a satellite as a state
> machine, implement it in haskell (14 locs) and use small check to verify
> that the state transitions fulfill the properties we expect for collision
> avoidance.
> >
> > - Model small sats as Monadic Stream Functions [1], implement a
> communication protocol on top (also using MSFs), and use quickcheck + fault
> injection to verify distributed consensus in the presence of faults. The
> next (immediate) step will be to bound the trace length and use smallcheck
> or something that exhausts the input space. I have also implemented Raft
> using MSFs, and the idea is to verify properties in a similar way.
> >
> > I know this is vague. Let me know if you have any questions or want more
> details.
>
> An appropriately vague response for a vague question! :)
>
> No, that's good, thanks.  I have considered using an FRP library for
> the _implementation_ but I couldn't really get my head around how I
> would use it for modelling and checking the protocol itself.


Well, the basic idea of MSFs is that they are just a function: MSF m a b =
a -> m (b, MSF m a b).

That means we can very easily prove properties about them. For example,
we've proven the arrow laws (
http://www.cs.nott.ac.uk/~psxip1/papers/msfmathprops.pdf). If you want to
mechanize proofs, it's helpful to have support for coinduction in your
language.


> I was
> considering reflex as it seems to be well regarded, and the
> browser/mobile capabilities appear to be good which could prove useful
> for me in the future.  I'm not sure how reflex is classified but I
> guess it's a 'classic' FRP system, so perhaps the issues I was facing
> would be analogous to those when using MSF/dunai.
>

Well, here my position would be a bit biased, of course. But there's good
reason why we created dunai. Our position with dunai is that there is a
more fundamental construct that a lot of existing ideas emerge from. We
have seen that many FRP implementations can functionally be expressed in
terms of MSFs, or MSFs + some extension (which you are more than welcome to
implement, since the library is extensible by design).

We use this for GUI-stuff. All the time. It's actually one of the initial
use cases that motivated creating dunai. Plus, you can run Yampa on top of
dunai. So, we have Yampa mobile games running linked using bearriver (a
Yampa-compatible FRP layer). Yampa (and dunai) also runs on the browser
(see the GHCjs branch of haskanoid). I have also a layer for the
GUI-oriented reactive library Keera Hails. It's quite fast too. For a
recent paper, I had to run complex physics simulations in Yampa, and this
was clocked at 60Hz rendering (vsync) and about 10000 simulation cycles per
frame (meaning 60K simulation cycles per second).

Even though MSFs look arrowized, an MSF with unit input is a stream, and
with time in the environment it is a signal. It's also a functor and an
applicative. So you can write the same classic FRP style, if you want.

Your email has made me take a second look at a FRP option, and I think
> I was seeing problems where there aren't any.
>
> One difficulty I perceived was the heterogeneity of the participants
> in the protocol and the multi-point communications, well beyond a
> simple sending/receiving distinction.
> That worries me less now.  It seems that if I could come up with a
> statechart description of each participant it's probably a fairly
> mechanical process to represent that in a FRP network.
> Perhaps that explains why I couldn't find many libraries to do with
> more 'elaborate' state representations (as in statecharts are more
> elaborate than FSM/automata/etc).  Maybe once you reach that
> complexity they're not the best way to think about the problem in
> Haskell.
>
> The 'complex heterogeneity' reinforced my main problem, which now I
> think might just be a case premature optimisation.  It seemed that if
> I wanted to enumerate all states while testing the protocol I would
> need to 'branch' each participant whenever they changed and
> recursively test each temporal alternative... and that probably
> involved building, modifying, reorganising, restoring networks on the
> fly.  Maybe achievable, but I couldn't immediately see how.  But a
> simple succession of root-to-tip searches/executions of that tree
> could be perfectly adequate.
> Just have to try it out but I think I was getting carried away.
>
> Anyway, after that additional vagueness... a bit of a tangent. :)
> One problem I have with the Haskell ecosystem is I end up falling down
> the rabbit-hole whenever I start researching something.  And within
> each rabbit-hole I find more
> interesting-thing-to-research-rabbit-holes, and within them... etc,
> etc.  Soon I'm so deep down the rabbit-holes I'm smothered in quantum
> foam and don't know which way is up.
> On my last foray I started with MSF and came upon Streamly:
> https://hackage.haskell.org/package/streamly-0.6.0
> Are you familiar with it?


I have not explored it yet. But it seems related. Just for info, there's a
package called Rhine that extends Dunai with type-safe parallelism and
asynchronicity. It ensures that communications specify buffers that are
compatible.

  To my inexperienced eye it seems quite
> similar to MSF/dunai, do you have any thoughts on it?  Relative merits
> in different use cases?
> Reflex appeals to me because of the possibility of learning it and
> leveraging it's UI layers in other projects.  But for a protocol
> implementation it feels like maybe I should be using something more,
> um... stripped back/fundamental.
>
> Again, thanks for the reply.
>

My pleasure! Let me know if you have any questions.

I'd recommend that you take a look at these papers:

- "FRP Refactored": https://dl.acm.org/citation.cfm?id=2976010 (the
original MSF paper, shows classic and arrowized FRP)
- "Rhine: FRP with type-level clocks":
https://dl.acm.org/citation.cfm?id=3242757 (asynchronicity, concurrency and
parallelism with MSFs)
- "Testing and debugging FRP": https://dl.acm.org/citation.cfm?id=3110246
(quickcheck + temporal logic + FRP)
- "Fault Tolerant FRP": https://dl.acm.org/citation.cfm?id=3236791

I'm happy to provide copies of these papers if you want them :) My website (
http://www.cs.nott.ac.uk/~psxip1/) should have links to all of them.

All the best,

Ivan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190310/d91140af/attachment.html>