Informal modelling and simulation of protocols

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
18 messages Options
Reply | Threaded
Open this post in threaded view
|

Informal modelling and simulation of protocols

P Orrifolius
Hi,

this will probably be a somewhat rambling, open-ended question... my
apologies in advance.
There are some concrete questions after I explain what I'm trying to
achieve, and some of them may even make sense!

I'm planning on writing a multi-party, distributed protocol.  I would
like to informally model the protocol itself and the environment it
would run in and then simulate it to see if it achieves what I expect.
Then it would need to be implemented and tested of course.
I think a formal, mathematical model of the protocol would be beyond
my abilities.

I'm looking for any advice or tool/library recommendations I can get
on the modelling and simulating part of the process and how that work
could be leveraged in the implementation to reduce the work and help
ensure correctness.


I have some ideas of how this could work, but I don't know if I'm
approaching it with a suitably Haskell-like mindset...
What I envisage at the moment is defining the possible behaviour of
each party, who are not homogeneous, as well as things which form the
external environment of the parties but will impact their behaviour.
By external things I mean, for example, communication links which may
drop or reorder packets, storage devices which may lose or corrupt
data, machines that freeze or slew their clock... that sort of thing.
I'm also picturing a 'universal coordinator' that controls interaction
of the parties/environment during simulation.

Modelling each party and external as a Harel-like statechart seems
plausible.  Perhaps some parts could be simpler FSMs, but I think many
will be reasonably complex and involve internal state.

It would be nice if the simulation could, to the limit of given
processing time, exhaustively check the model rather than just
randomly, as per quickcheck.
If at each point the universal coordinator got a list of possible next
states from each party/external it could simulate the
simultaneity/sequencing of events by enumerating all combinations, of
every size, of individual party/external transitions and then
recursing with each separate combination applied as being the next set
of simultaneous state transitions.

To reduce the space to exhaustively search it would be nice if any
values that the parties used, and were being tested by, were
abstracted.  Not sure what the technical term is but I mean asserting
relationships between variables in a given domain, rather than their
actual value.
For example, imagine a distributed vote between two nodes where each
node must vote for a random integer greater than their last vote.
Each node is a party in the protocol.
In the current branch of the exhaustive search of the protocol a
relation between node 1's existing vote, v1, and node 2's existing
vote, v2, has already been asserted: v1>v2.
So when the coordinator enumerates the possibilities for sets of
next-state transitions, with each node n asserting vn'>vn in their
individual party state transition, it will prune any search branch
which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,
v2'>v2), and recurse into the search branch alternatives with v1'<v2',
or v1'=v2', or v1'>v2'.



So, some questions...

Is what I'm suggesting even vaguely sensible way to approach the
problem in Haskell?  Or am I getting carried away and some neat tricks
zipping list monoids or something will get the job done?

Is there some fantastic tool/library which already does everything I want?

Are there any good tools or libraries in Haskell for defining and
manipulating statecharts?

The sessiontypes, and sessiontypes-distributed, libraries are cool,
representing the protocol at the type level... but these only handle
point-to-point, two-party protocols, right?
I expect that extending them would be a _serious_ amount of work.

Can quickcheck do the sort of exhaustive coverage testing that I'd like?

Again, not sure of the correct terminology but can quickcheck generate
tests at a variable-relation assertion level?  I.e. inspect the
operators and boolean tests over a domain (+, ==, >=, append, length,
contains, etc) and explore test cases according to whether certain
relations between variables hold.

Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless
Final Interpreter (http://okmij.org/ftp/tagless-final/index.html) work
might be a useful mechanism to define the behaviour of parties within
the protocol (the statecharts, basically) and then have different
interpreters that enable both the testing  and implementation of the
protocol, to keep them more closely aligned?
I read that work years ago and have wanted to try it out ever since,
so I may be overlooking the fact that it's totally unsuitable!
Perhaps superseded now, but if it can allow more of the protocol to be
expressed at the type level that would be good.


Yeah, rambling.  Sorry about that.


Thanks!
porrifolius
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Doug McIlroy

> Is there some fantastic tool/library which already does everything I want?

Have you looked into model checkers like Spin, which was developed
for the very purpose of exhaustively checking protocols? See spinroot.com

Doug McIlroy
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Will Yager

On Mar 4, 2019, at 10:33 PM, Doug McIlroy <[hidden email]> wrote:


Is there some fantastic tool/library which already does everything I want?

Have you looked into model checkers like Spin, which was developed
for the very purpose of exhaustively checking protocols? See spinroot.com

Doug McIlroy
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Ivan Perez
In reply to this post by P Orrifolius
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.

Ivan


On Mon, 4 Mar 2019 at 02:05, P Orrifolius <[hidden email]> wrote:
Hi,

this will probably be a somewhat rambling, open-ended question... my
apologies in advance.
There are some concrete questions after I explain what I'm trying to
achieve, and some of them may even make sense!

I'm planning on writing a multi-party, distributed protocol.  I would
like to informally model the protocol itself and the environment it
would run in and then simulate it to see if it achieves what I expect.
Then it would need to be implemented and tested of course.
I think a formal, mathematical model of the protocol would be beyond
my abilities.

I'm looking for any advice or tool/library recommendations I can get
on the modelling and simulating part of the process and how that work
could be leveraged in the implementation to reduce the work and help
ensure correctness.


I have some ideas of how this could work, but I don't know if I'm
approaching it with a suitably Haskell-like mindset...
What I envisage at the moment is defining the possible behaviour of
each party, who are not homogeneous, as well as things which form the
external environment of the parties but will impact their behaviour.
By external things I mean, for example, communication links which may
drop or reorder packets, storage devices which may lose or corrupt
data, machines that freeze or slew their clock... that sort of thing.
I'm also picturing a 'universal coordinator' that controls interaction
of the parties/environment during simulation.

Modelling each party and external as a Harel-like statechart seems
plausible.  Perhaps some parts could be simpler FSMs, but I think many
will be reasonably complex and involve internal state.

It would be nice if the simulation could, to the limit of given
processing time, exhaustively check the model rather than just
randomly, as per quickcheck.
If at each point the universal coordinator got a list of possible next
states from each party/external it could simulate the
simultaneity/sequencing of events by enumerating all combinations, of
every size, of individual party/external transitions and then
recursing with each separate combination applied as being the next set
of simultaneous state transitions.

To reduce the space to exhaustively search it would be nice if any
values that the parties used, and were being tested by, were
abstracted.  Not sure what the technical term is but I mean asserting
relationships between variables in a given domain, rather than their
actual value.
For example, imagine a distributed vote between two nodes where each
node must vote for a random integer greater than their last vote.
Each node is a party in the protocol.
In the current branch of the exhaustive search of the protocol a
relation between node 1's existing vote, v1, and node 2's existing
vote, v2, has already been asserted: v1>v2.
So when the coordinator enumerates the possibilities for sets of
next-state transitions, with each node n asserting vn'>vn in their
individual party state transition, it will prune any search branch
which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,
v2'>v2), and recurse into the search branch alternatives with v1'<v2',
or v1'=v2', or v1'>v2'.



So, some questions...

Is what I'm suggesting even vaguely sensible way to approach the
problem in Haskell?  Or am I getting carried away and some neat tricks
zipping list monoids or something will get the job done?

Is there some fantastic tool/library which already does everything I want?

Are there any good tools or libraries in Haskell for defining and
manipulating statecharts?

The sessiontypes, and sessiontypes-distributed, libraries are cool,
representing the protocol at the type level... but these only handle
point-to-point, two-party protocols, right?
I expect that extending them would be a _serious_ amount of work.

Can quickcheck do the sort of exhaustive coverage testing that I'd like?

Again, not sure of the correct terminology but can quickcheck generate
tests at a variable-relation assertion level?  I.e. inspect the
operators and boolean tests over a domain (+, ==, >=, append, length,
contains, etc) and explore test cases according to whether certain
relations between variables hold.

Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless
Final Interpreter (http://okmij.org/ftp/tagless-final/index.html) work
might be a useful mechanism to define the behaviour of parties within
the protocol (the statecharts, basically) and then have different
interpreters that enable both the testing  and implementation of the
protocol, to keep them more closely aligned?
I read that work years ago and have wanted to try it out ever since,
so I may be overlooking the fact that it's totally unsuitable!
Perhaps superseded now, but if it can allow more of the protocol to be
expressed at the type level that would be good.


Yeah, rambling.  Sorry about that.


Thanks!
porrifolius
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Carter Schonwald
In reply to this post by P Orrifolius
TLA plus might suit you! I've actually had some success going back and forth between copattern style code and TLA specs, its not easy and not perfect, but it works

i've been slowly experimenting with modelling protocols as coinductive / copattern style trick 

i am messing around with some reusable abstractions, though its definitely a challenging problem 

On Mon, Mar 4, 2019 at 2:05 AM P Orrifolius <[hidden email]> wrote:
Hi,

this will probably be a somewhat rambling, open-ended question... my
apologies in advance.
There are some concrete questions after I explain what I'm trying to
achieve, and some of them may even make sense!

I'm planning on writing a multi-party, distributed protocol.  I would
like to informally model the protocol itself and the environment it
would run in and then simulate it to see if it achieves what I expect.
Then it would need to be implemented and tested of course.
I think a formal, mathematical model of the protocol would be beyond
my abilities.

I'm looking for any advice or tool/library recommendations I can get
on the modelling and simulating part of the process and how that work
could be leveraged in the implementation to reduce the work and help
ensure correctness.


I have some ideas of how this could work, but I don't know if I'm
approaching it with a suitably Haskell-like mindset...
What I envisage at the moment is defining the possible behaviour of
each party, who are not homogeneous, as well as things which form the
external environment of the parties but will impact their behaviour.
By external things I mean, for example, communication links which may
drop or reorder packets, storage devices which may lose or corrupt
data, machines that freeze or slew their clock... that sort of thing.
I'm also picturing a 'universal coordinator' that controls interaction
of the parties/environment during simulation.

Modelling each party and external as a Harel-like statechart seems
plausible.  Perhaps some parts could be simpler FSMs, but I think many
will be reasonably complex and involve internal state.

It would be nice if the simulation could, to the limit of given
processing time, exhaustively check the model rather than just
randomly, as per quickcheck.
If at each point the universal coordinator got a list of possible next
states from each party/external it could simulate the
simultaneity/sequencing of events by enumerating all combinations, of
every size, of individual party/external transitions and then
recursing with each separate combination applied as being the next set
of simultaneous state transitions.

To reduce the space to exhaustively search it would be nice if any
values that the parties used, and were being tested by, were
abstracted.  Not sure what the technical term is but I mean asserting
relationships between variables in a given domain, rather than their
actual value.
For example, imagine a distributed vote between two nodes where each
node must vote for a random integer greater than their last vote.
Each node is a party in the protocol.
In the current branch of the exhaustive search of the protocol a
relation between node 1's existing vote, v1, and node 2's existing
vote, v2, has already been asserted: v1>v2.
So when the coordinator enumerates the possibilities for sets of
next-state transitions, with each node n asserting vn'>vn in their
individual party state transition, it will prune any search branch
which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,
v2'>v2), and recurse into the search branch alternatives with v1'<v2',
or v1'=v2', or v1'>v2'.



So, some questions...

Is what I'm suggesting even vaguely sensible way to approach the
problem in Haskell?  Or am I getting carried away and some neat tricks
zipping list monoids or something will get the job done?

Is there some fantastic tool/library which already does everything I want?

Are there any good tools or libraries in Haskell for defining and
manipulating statecharts?

The sessiontypes, and sessiontypes-distributed, libraries are cool,
representing the protocol at the type level... but these only handle
point-to-point, two-party protocols, right?
I expect that extending them would be a _serious_ amount of work.

Can quickcheck do the sort of exhaustive coverage testing that I'd like?

Again, not sure of the correct terminology but can quickcheck generate
tests at a variable-relation assertion level?  I.e. inspect the
operators and boolean tests over a domain (+, ==, >=, append, length,
contains, etc) and explore test cases according to whether certain
relations between variables hold.

Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless
Final Interpreter (http://okmij.org/ftp/tagless-final/index.html) work
might be a useful mechanism to define the behaviour of parties within
the protocol (the statecharts, basically) and then have different
interpreters that enable both the testing  and implementation of the
protocol, to keep them more closely aligned?
I read that work years ago and have wanted to try it out ever since,
so I may be overlooking the fact that it's totally unsuitable!
Perhaps superseded now, but if it can allow more of the protocol to be
expressed at the type level that would be good.


Yeah, rambling.  Sorry about that.


Thanks!
porrifolius
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Kaushik Chakraborty
In reply to this post by Ivan Perez
Hi,

- 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 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
)? Is there some reference code that you can share.
Thanks in advance.



On Tue, Mar 5, 2019, at 19:00, Ivan Perez 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.

Ivan


On Mon, 4 Mar 2019 at 02:05, P Orrifolius <[hidden email]> wrote:
Hi,

this will probably be a somewhat rambling, open-ended question... my
apologies in advance.
There are some concrete questions after I explain what I'm trying to
achieve, and some of them may even make sense!

I'm planning on writing a multi-party, distributed protocol.  I would
like to informally model the protocol itself and the environment it
would run in and then simulate it to see if it achieves what I expect.
Then it would need to be implemented and tested of course.
I think a formal, mathematical model of the protocol would be beyond
my abilities.

I'm looking for any advice or tool/library recommendations I can get
on the modelling and simulating part of the process and how that work
could be leveraged in the implementation to reduce the work and help
ensure correctness.


I have some ideas of how this could work, but I don't know if I'm
approaching it with a suitably Haskell-like mindset...
What I envisage at the moment is defining the possible behaviour of
each party, who are not homogeneous, as well as things which form the
external environment of the parties but will impact their behaviour.
By external things I mean, for example, communication links which may
drop or reorder packets, storage devices which may lose or corrupt
data, machines that freeze or slew their clock... that sort of thing.
I'm also picturing a 'universal coordinator' that controls interaction
of the parties/environment during simulation.

Modelling each party and external as a Harel-like statechart seems
plausible.  Perhaps some parts could be simpler FSMs, but I think many
will be reasonably complex and involve internal state.

It would be nice if the simulation could, to the limit of given
processing time, exhaustively check the model rather than just
randomly, as per quickcheck.
If at each point the universal coordinator got a list of possible next
states from each party/external it could simulate the
simultaneity/sequencing of events by enumerating all combinations, of
every size, of individual party/external transitions and then
recursing with each separate combination applied as being the next set
of simultaneous state transitions.

To reduce the space to exhaustively search it would be nice if any
values that the parties used, and were being tested by, were
abstracted.  Not sure what the technical term is but I mean asserting
relationships between variables in a given domain, rather than their
actual value.
For example, imagine a distributed vote between two nodes where each
node must vote for a random integer greater than their last vote.
Each node is a party in the protocol.
In the current branch of the exhaustive search of the protocol a
relation between node 1's existing vote, v1, and node 2's existing
vote, v2, has already been asserted: v1>v2.
So when the coordinator enumerates the possibilities for sets of
next-state transitions, with each node n asserting vn'>vn in their
individual party state transition, it will prune any search branch
which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,
v2'>v2), and recurse into the search branch alternatives with v1'<v2',
or v1'=v2', or v1'>v2'.



So, some questions...

Is what I'm suggesting even vaguely sensible way to approach the
problem in Haskell?  Or am I getting carried away and some neat tricks
zipping list monoids or something will get the job done?

Is there some fantastic tool/library which already does everything I want?

Are there any good tools or libraries in Haskell for defining and
manipulating statecharts?

The sessiontypes, and sessiontypes-distributed, libraries are cool,
representing the protocol at the type level... but these only handle
point-to-point, two-party protocols, right?
I expect that extending them would be a _serious_ amount of work.

Can quickcheck do the sort of exhaustive coverage testing that I'd like?

Again, not sure of the correct terminology but can quickcheck generate
tests at a variable-relation assertion level?  I.e. inspect the
operators and boolean tests over a domain (+, ==, >=, append, length,
contains, etc) and explore test cases according to whether certain
relations between variables hold.

Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless
might be a useful mechanism to define the behaviour of parties within
the protocol (the statecharts, basically) and then have different
interpreters that enable both the testing  and implementation of the
protocol, to keep them more closely aligned?
I read that work years ago and have wanted to try it out ever since,
so I may be overlooking the fact that it's totally unsuitable!
Perhaps superseded now, but if it can allow more of the protocol to be
expressed at the type level that would be good.


Yeah, rambling.  Sorry about that.


Thanks!
porrifolius
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Ian Denhardt
In reply to this post by P Orrifolius
This library may be of interest:

    https://hackage.haskell.org/package/dejafu

Quoting P Orrifolius (2019-03-04 02:05:06)

> Hi,
>
> this will probably be a somewhat rambling, open-ended question... my
> apologies in advance.
> There are some concrete questions after I explain what I'm trying to
> achieve, and some of them may even make sense!
>
> I'm planning on writing a multi-party, distributed protocol.  I would
> like to informally model the protocol itself and the environment it
> would run in and then simulate it to see if it achieves what I expect.
> Then it would need to be implemented and tested of course.
> I think a formal, mathematical model of the protocol would be beyond
> my abilities.
>
> I'm looking for any advice or tool/library recommendations I can get
> on the modelling and simulating part of the process and how that work
> could be leveraged in the implementation to reduce the work and help
> ensure correctness.
>
>
> I have some ideas of how this could work, but I don't know if I'm
> approaching it with a suitably Haskell-like mindset...
> What I envisage at the moment is defining the possible behaviour of
> each party, who are not homogeneous, as well as things which form the
> external environment of the parties but will impact their behaviour.
> By external things I mean, for example, communication links which may
> drop or reorder packets, storage devices which may lose or corrupt
> data, machines that freeze or slew their clock... that sort of thing.
> I'm also picturing a 'universal coordinator' that controls interaction
> of the parties/environment during simulation.
>
> Modelling each party and external as a Harel-like statechart seems
> plausible.  Perhaps some parts could be simpler FSMs, but I think many
> will be reasonably complex and involve internal state.
>
> It would be nice if the simulation could, to the limit of given
> processing time, exhaustively check the model rather than just
> randomly, as per quickcheck.
> If at each point the universal coordinator got a list of possible next
> states from each party/external it could simulate the
> simultaneity/sequencing of events by enumerating all combinations, of
> every size, of individual party/external transitions and then
> recursing with each separate combination applied as being the next set
> of simultaneous state transitions.
>
> To reduce the space to exhaustively search it would be nice if any
> values that the parties used, and were being tested by, were
> abstracted.  Not sure what the technical term is but I mean asserting
> relationships between variables in a given domain, rather than their
> actual value.
> For example, imagine a distributed vote between two nodes where each
> node must vote for a random integer greater than their last vote.
> Each node is a party in the protocol.
> In the current branch of the exhaustive search of the protocol a
> relation between node 1's existing vote, v1, and node 2's existing
> vote, v2, has already been asserted: v1>v2.
> So when the coordinator enumerates the possibilities for sets of
> next-state transitions, with each node n asserting vn'>vn in their
> individual party state transition, it will prune any search branch
> which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,
> v2'>v2), and recurse into the search branch alternatives with v1'<v2',
> or v1'=v2', or v1'>v2'.
>
>
>
> So, some questions...
>
> Is what I'm suggesting even vaguely sensible way to approach the
> problem in Haskell?  Or am I getting carried away and some neat tricks
> zipping list monoids or something will get the job done?
>
> Is there some fantastic tool/library which already does everything I want?
>
> Are there any good tools or libraries in Haskell for defining and
> manipulating statecharts?
>
> The sessiontypes, and sessiontypes-distributed, libraries are cool,
> representing the protocol at the type level... but these only handle
> point-to-point, two-party protocols, right?
> I expect that extending them would be a _serious_ amount of work.
>
> Can quickcheck do the sort of exhaustive coverage testing that I'd like?
>
> Again, not sure of the correct terminology but can quickcheck generate
> tests at a variable-relation assertion level?  I.e. inspect the
> operators and boolean tests over a domain (+, ==, >=, append, length,
> contains, etc) and explore test cases according to whether certain
> relations between variables hold.
>
> Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless
> Final Interpreter (http://okmij.org/ftp/tagless-final/index.html) work
> might be a useful mechanism to define the behaviour of parties within
> the protocol (the statecharts, basically) and then have different
> interpreters that enable both the testing  and implementation of the
> protocol, to keep them more closely aligned?
> I read that work years ago and have wanted to try it out ever since,
> so I may be overlooking the fact that it's totally unsuitable!
> Perhaps superseded now, but if it can allow more of the protocol to be
> expressed at the type level that would be good.
>
>
> Yeah, rambling.  Sorry about that.
>
>
> Thanks!
> porrifolius
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

MarLinn
In reply to this post by Ivan Perez
2cents:

AFAIK in existing general-purpose simulation frameworks the type of
simulation you need for this type of problem is typically implemented in
a way that very closely resembles "classical" FRP, particularly it's
definition of events. The framework basically manages huge queues of
time-action-pairs.

So several of the FRP libraries might be a good candidate. I haven't had
a chance to experiment with MSF's yet, but seeing as they are a
development in FRP space, Ivan's approach sounds like quite a good idea.

Cheers.

On 05/03/2019 14.29, Ivan Perez 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.
>
> Ivan
>
> [1] https://github.com/ivanperez-keera/dunai
> [2] https://arc.aiaa.org/doi/abs/10.2514/6.2019-1187

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by Doug McIlroy
On Tue, 5 Mar 2019 at 03:33, Doug McIlroy <[hidden email]> wrote:
>
>
> > Is there some fantastic tool/library which already does everything I want?
>
> Have you looked into model checkers like Spin, which was developed
> for the very purpose of exhaustively checking protocols? See spinroot.com

Thanks for lead.  Spin does seem to be an appropriate tool for the job.

I was/am sort of hoping the protocol modelling and implementation
would both be in Haskell to get some reuse, but the consensus seems to
be that Spin's modelling language is pretty easy to use so maybe it
would  be no extra work overall.

I'm sure I've still got the implementation and protocol itself
somewhat confused, so what state is truly required for the protocol is
a bit muddled.  Not certain how I would represent it in spin, just
need to play around with it I guess.
That's partly what I was getting at with my 'modelling operators over
domains' ramble... trying to avoid increasing the state space by
enumerating through all data type values without abstracting the
protocol model by just checking boundary cases.  Or at least
abstracting in a disciplined way that makes me confident all boundary
cases are checked, not just those I happened to think of and model.
But perhaps Spin already has some state space compression tricks of
that nature and I'm worrying over nothing.

Anyway, thanks for the pointer!
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by Ivan Perez
On Wed, 6 Mar 2019 at 02:30, Ivan Perez <[hidden email]> 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.  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.

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?  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.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by Will Yager
Hi, Will (and Ian)

On Tue, 5 Mar 2019 at 23:11, Will Yager <[hidden email]> wrote:
>
> http://hackage.haskell.org/package/dejafu might do what you want

Thanks for the suggestion, that does look useful.
From a quick look at the documentation... am I right in thinking that
this test framework only covers concurrency when you're directly using
IOVars and STM?  Any concurrency that might involve other primitives,
or IOVar/STM uses in libraries, wouldn't be testable?  Unless the
primitives/library had also been written to use the dejafu io classes
and monads of course... which might be a good idea in and of itself.
Definitely looks good for helping ensure correctness at my protocol
implementation layer, and I can conceive of building a protocol model
testable by it, so thanks for the link.  Need to think more about the
relative merits of that approach vs Spin vs FRP.

Thanks.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by Carter Schonwald
On Wed, 6 Mar 2019 at 06:00, Carter Schonwald
<[hidden email]> wrote:
>
> TLA plus might suit you! I've actually had some success going back and forth between copattern style code and TLA specs, its not easy and not perfect, but it works
>
> i've been slowly experimenting with modelling protocols as coinductive / copattern style trick
> https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/ is a small toy exposition i did
>
> i am messing around with some reusable abstractions, though its definitely a challenging problem

I will be honest and confess that I can't get my head around it.  Not
your fault though! :)

I think I have a basic understanding of
co-(recursion|induction|patterns) so, at a lay-person's level of
understanding, can I conceptually think of these things as streams
very similar to, for example, those processed by the Monadic Stream
Functions that Ivan Perez mentions in another email?
And then there is some additional analytical or performance
advantages, maybe especially in cases of infinite streams, achieved by
representing them in this manner?

I think I'll need to study up to really appreciate it but, at the very
least, I'm thankful for the link to your post as your reference to the
machines library led me off down an interesting research rabbit-hole.
:)
Thanks!
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by Kaushik Chakraborty
On Thu, 7 Mar 2019 at 14:14, Kaushik Chakraborty
<[hidden email]> wrote:
>
> Hi,
>
> - 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 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
> )? Is there some reference code that you can share.
> Thanks in advance.

I'm interested in that part of the system as well.  For what it's
worth I was envisaging explicitly modelling each external
process/component that could experience faults so that I could
enumerate those failure states, and all combinations of them,
exhaustively.  I've also given passing thought to modelling faults
within the internal processes so I could see what happens when dealing
with Byzantine failures.
Definitely something I should read up on.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Ivan Perez
In reply to this post by P Orrifolius


On Sun, 10 Mar 2019 at 20:20, P Orrifolius <[hidden email]> wrote:
On Wed, 6 Mar 2019 at 02:30, Ivan Perez <[hidden email]> 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)

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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by MarLinn
On Fri, 8 Mar 2019 at 02:28, MarLinn <[hidden email]> wrote:

> AFAIK in existing general-purpose simulation frameworks the type of
> simulation you need for this type of problem is typically implemented in
> a way that very closely resembles "classical" FRP, particularly it's
> definition of events. The framework basically manages huge queues of
> time-action-pairs.

Interesting.  So it's possible that the Spin model checker takes a
similar approach, along with all sorts of state-space compression
tricks and such like.

> So several of the FRP libraries might be a good candidate. I haven't had
> a chance to experiment with MSF's yet, but seeing as they are a
> development in FRP space, Ivan's approach sounds like quite a good idea.

I am coming (back) around to some sort of FRP modelling... it'd be
hubris to expect to top Spin, but as long as I'm learning it's fine I
suppose.
It appears to me now that a FRP network of streams may allow quite a
lot of re-use between protocol modelling and implementation... it may
be pretty straight forward to substitute the 2 alternative
sub-networks of the modelling FRP that carried out "receive (good|bad)
message -> emit message count+(1|0)" with the implementation "receive
message -> check signature -> write to disk -> etc -> emit message
count+(1|0)".

And it occurs to me now that using CRDTs, and Lamport or vector
clocks, to manage variables/state on the individual simulation runs
could provide quite an effective state-space compression, collapse the
tree of runs down to a graph.


Thanks for the 2 cents.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

P Orrifolius
In reply to this post by Ivan Perez
On Mon, 11 Mar 2019 at 14:45, Ivan Perez <[hidden email]> wrote:
>
> My pleasure! Let me know if you have any questions.

I dare say I will. :)
Lots of pointers there, I'll take a look and try to digest it.  A
couple of points there that are already correcting/clarifying things
for me I think.

I see more quantum foam in my future... but I appreciate the help
nonetheless.  Thanks! :)
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Ian Denhardt
In reply to this post by P Orrifolius
Quoting P Orrifolius (2019-03-10 20:38:05)

> On Tue, 5 Mar 2019 at 23:11, Will Yager <[hidden email]> wrote:
> >
> > http://hackage.haskell.org/package/dejafu might do what you want
>
> Thanks for the suggestion, that does look useful.
> From a quick look at the documentation... am I right in thinking that
> this test framework only covers concurrency when you're directly using
> IOVars and STM?  Any concurrency that might involve other primitives,
> or IOVar/STM uses in libraries, wouldn't be testable?  Unless the
> primitives/library had also been written to use the dejafu io classes
> and monads of course... which might be a good idea in and of itself.

Yeah, if you have dependencies not written in terms of those type
classes, it may be difficult to integrate. If it's just your own code,
it shouldn't be too hard to go through and swap in the type class
constraints everywhere, but I do wish Haskell made it easier to wedge
an abstraction layer like that under existing libraries after the fact
:(.

-Ian
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Informal modelling and simulation of protocols

Michael Walker
In reply to this post by P Orrifolius
Hi,
 
On Tue, 5 Mar 2019 at 23:11, Will Yager <[hidden email]> wrote:
>
> http://hackage.haskell.org/package/dejafu might do what you want

Thanks for the suggestion, that does look useful.
From a quick look at the documentation... am I right in thinking that
this test framework only covers concurrency when you're directly using
IOVars and STM?  Any concurrency that might involve other primitives,
or IOVar/STM uses in libraries, wouldn't be testable?  Unless the
primitives/library had also been written to use the dejafu io classes
and monads of course... which might be a good idea in and of itself.

Yes, that's the case.  It's a bit of an unfortunate limitation but I don't currently have a way around it.

You may find it interesting to look at adjoint.io's libraft, which uses dejafu for some tests: https://github.com/adjoint-io/raft/blob/master/test/TestDejaFu.hs

The way they do it is by writing their library in terms of some "MonadRaft" classes, and give a concrete implementation of those classes in terms of dejafu's ConcIO monad for testing. 

--

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.