<!DOCTYPE html><html><head><title></title><style type="text/css">p.MsoNormal,p.MsoNoSpacing{margin:0}</style></head><body><div style="font-family:Arial;">Hi,<br></div><div style="font-family:Arial;"><br></div><blockquote type="cite"><div style="font-family:Arial;">-
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.<br></div></blockquote><div style="font-family:Arial;"><br></div><div style="font-family:Arial;"><div style="font-family:Arial;">I
am interested to know the "fault injection" part. Did you inject the
same randomly as in general Chaos Engg style or used formal techniques
like LDFI (lineage driven fault injection<br></div><div style="font-family:Arial;">)? Is there some reference code that you can share. <br></div><div style="font-family:Arial;">Thanks in advance. <br></div><div style="font-family:Arial;"><br></div></div><div id="defanged59-sig18407013"><div class="defanged59-signature">Cheers!<br></div><div class="defanged59-signature">Kaushik<br></div><div class="defanged59-signature"><a href="https://keybase.io/kaushikc/" rel="noopener noreferrer">https://keybase.io/kaushikc/</a><br></div></div><div style="font-family:Arial;"><br></div><div style="font-family:Arial;"><br></div><div style="font-family:Arial;">On Tue, Mar 5, 2019, at 19:00, Ivan Perez wrote:<br></div><blockquote type="cite" id="fastmail-quoted"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Hi<br></div><div><br></div><div>Partly related; for recent work we did two things:<br></div><div><br></div><div>- 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.<br></div><div><br></div><div>- 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.<br></div><div><br></div><div>I know this is vague. Let me know if you have any questions or want more details.<br></div><div><br></div><div>Ivan<br></div><div><br></div><div>[1] <a href="https://github.com/ivanperez-keera/dunai">https://github.com/ivanperez-keera/dunai</a><br></div><div>[2] <a href="https://arc.aiaa.org/doi/abs/10.2514/6.2019-1187">https://arc.aiaa.org/doi/abs/10.2514/6.2019-1187</a><br></div></div></div></div><div style="font-family:Arial;"><br></div><div class="fastmail-quoted-gmail_quote"><div class="fastmail-quoted-gmail_attr" dir="ltr">On Mon, 4 Mar 2019 at 02:05, P Orrifolius <<a href="mailto:porrifolius@gmail.com">porrifolius@gmail.com</a>> wrote:<br></div><blockquote style="margin-top:0px;margin-right:0px;margin-bottom:0px;margin-left:0.8ex;border-left-color:rgb(204, 204, 204);border-left-style:solid;border-left-width:1px;padding-left:1ex;" class="fastmail-quoted-gmail_quote"><div style="font-family:Arial;">Hi,<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> this will probably be a somewhat rambling, open-ended question... my<br></div><div style="font-family:Arial;"> apologies in advance.<br></div><div style="font-family:Arial;"> There are some concrete questions after I explain what I'm trying to<br></div><div style="font-family:Arial;"> achieve, and some of them may even make sense!<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> I'm planning on writing a multi-party, distributed protocol. I would<br></div><div style="font-family:Arial;"> like to informally model the protocol itself and the environment it<br></div><div style="font-family:Arial;"> would run in and then simulate it to see if it achieves what I expect.<br></div><div style="font-family:Arial;"> Then it would need to be implemented and tested of course.<br></div><div style="font-family:Arial;"> I think a formal, mathematical model of the protocol would be beyond<br></div><div style="font-family:Arial;"> my abilities.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> I'm looking for any advice or tool/library recommendations I can get<br></div><div style="font-family:Arial;"> on the modelling and simulating part of the process and how that work<br></div><div style="font-family:Arial;"> could be leveraged in the implementation to reduce the work and help<br></div><div style="font-family:Arial;"> ensure correctness.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> I have some ideas of how this could work, but I don't know if I'm<br></div><div style="font-family:Arial;"> approaching it with a suitably Haskell-like mindset...<br></div><div style="font-family:Arial;"> What I envisage at the moment is defining the possible behaviour of<br></div><div style="font-family:Arial;"> each party, who are not homogeneous, as well as things which form the<br></div><div style="font-family:Arial;"> external environment of the parties but will impact their behaviour.<br></div><div style="font-family:Arial;"> By external things I mean, for example, communication links which may<br></div><div style="font-family:Arial;"> drop or reorder packets, storage devices which may lose or corrupt<br></div><div style="font-family:Arial;"> data, machines that freeze or slew their clock... that sort of thing.<br></div><div style="font-family:Arial;"> I'm also picturing a 'universal coordinator' that controls interaction<br></div><div style="font-family:Arial;"> of the parties/environment during simulation.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Modelling each party and external as a Harel-like statechart seems<br></div><div style="font-family:Arial;"> plausible. Perhaps some parts could be simpler FSMs, but I think many<br></div><div style="font-family:Arial;"> will be reasonably complex and involve internal state.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> It would be nice if the simulation could, to the limit of given<br></div><div style="font-family:Arial;"> processing time, exhaustively check the model rather than just<br></div><div style="font-family:Arial;"> randomly, as per quickcheck.<br></div><div style="font-family:Arial;"> If at each point the universal coordinator got a list of possible next<br></div><div style="font-family:Arial;"> states from each party/external it could simulate the<br></div><div style="font-family:Arial;"> simultaneity/sequencing of events by enumerating all combinations, of<br></div><div style="font-family:Arial;"> every size, of individual party/external transitions and then<br></div><div style="font-family:Arial;"> recursing with each separate combination applied as being the next set<br></div><div style="font-family:Arial;"> of simultaneous state transitions.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> To reduce the space to exhaustively search it would be nice if any<br></div><div style="font-family:Arial;"> values that the parties used, and were being tested by, were<br></div><div style="font-family:Arial;"> abstracted. Not sure what the technical term is but I mean asserting<br></div><div style="font-family:Arial;"> relationships between variables in a given domain, rather than their<br></div><div style="font-family:Arial;"> actual value.<br></div><div style="font-family:Arial;"> For example, imagine a distributed vote between two nodes where each<br></div><div style="font-family:Arial;"> node must vote for a random integer greater than their last vote.<br></div><div style="font-family:Arial;"> Each node is a party in the protocol.<br></div><div style="font-family:Arial;"> In the current branch of the exhaustive search of the protocol a<br></div><div style="font-family:Arial;"> relation between node 1's existing vote, v1, and node 2's existing<br></div><div style="font-family:Arial;"> vote, v2, has already been asserted: v1>v2.<br></div><div style="font-family:Arial;"> So when the coordinator enumerates the possibilities for sets of<br></div><div style="font-family:Arial;"> next-state transitions, with each node n asserting vn'>vn in their<br></div><div style="font-family:Arial;"> individual party state transition, it will prune any search branch<br></div><div style="font-family:Arial;"> which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,<br></div><div style="font-family:Arial;"> v2'>v2), and recurse into the search branch alternatives with v1'<v2',<br></div><div style="font-family:Arial;"> or v1'=v2', or v1'>v2'.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> So, some questions...<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Is what I'm suggesting even vaguely sensible way to approach the<br></div><div style="font-family:Arial;"> problem in Haskell? Or am I getting carried away and some neat tricks<br></div><div style="font-family:Arial;"> zipping list monoids or something will get the job done?<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Is there some fantastic tool/library which already does everything I want?<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Are there any good tools or libraries in Haskell for defining and<br></div><div style="font-family:Arial;"> manipulating statecharts?<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> The sessiontypes, and sessiontypes-distributed, libraries are cool,<br></div><div style="font-family:Arial;"> representing the protocol at the type level... but these only handle<br></div><div style="font-family:Arial;"> point-to-point, two-party protocols, right?<br></div><div style="font-family:Arial;"> I expect that extending them would be a _serious_ amount of work.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Can quickcheck do the sort of exhaustive coverage testing that I'd like?<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Again, not sure of the correct terminology but can quickcheck generate<br></div><div style="font-family:Arial;"> tests at a variable-relation assertion level? I.e. inspect the<br></div><div style="font-family:Arial;"> operators and boolean tests over a domain (+, ==, >=, append, length,<br></div><div style="font-family:Arial;"> contains, etc) and explore test cases according to whether certain<br></div><div style="font-family:Arial;"> relations between variables hold.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless<br></div><div style="font-family:Arial;"> Final Interpreter (<a rel="noreferrer" href="http://okmij.org/ftp/tagless-final/index.html">http://okmij.org/ftp/tagless-final/index.html</a>) work<br></div><div style="font-family:Arial;"> might be a useful mechanism to define the behaviour of parties within<br></div><div style="font-family:Arial;"> the protocol (the statecharts, basically) and then have different<br></div><div style="font-family:Arial;"> interpreters that enable both the testing and implementation of the<br></div><div style="font-family:Arial;"> protocol, to keep them more closely aligned?<br></div><div style="font-family:Arial;"> I read that work years ago and have wanted to try it out ever since,<br></div><div style="font-family:Arial;"> so I may be overlooking the fact that it's totally unsuitable!<br></div><div style="font-family:Arial;"> Perhaps superseded now, but if it can allow more of the protocol to be<br></div><div style="font-family:Arial;"> expressed at the type level that would be good.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Yeah, rambling. Sorry about that.<br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> <br></div><div style="font-family:Arial;"> Thanks!<br></div><div style="font-family:Arial;"> porrifolius<br></div><div style="font-family:Arial;"> _______________________________________________<br></div><div style="font-family:Arial;"> Haskell-Cafe mailing list<br></div><div style="font-family:Arial;"> To (un)subscribe, modify options or view archives go to:<br></div><div style="font-family:Arial;"> <a rel="noreferrer" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br></div><div style="font-family:Arial;"> Only members subscribed via the mailman list are allowed to post.<br></div></blockquote></div><div>_______________________________________________<br></div><div>Haskell-Cafe mailing list<br></div><div>To (un)subscribe, modify options or view archives go to:<br></div><div>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe<br></div><div>Only members subscribed via the mailman list are allowed to post.<br></div></blockquote><div style="font-family:Arial;"><br></div></body></html>