use lvish

[gelisam]

We claim that our implementation doesn't depend on the order in which the tasks are scheduled, but we've never proved it. We sometimes mention the lvish library as an analogy, explaining that the reason we think our claim is true is that all of our side-effects move our state up a lattice of information.

Using lvish (as opposed to just mentioning it) would allow us to:

• build on lvish's proof of correctness to drastically simplify our proof effort
• it would allow us to add new builtins more confidently, because lvish will check that we are not breaking our claim.
• speed up the implementation by using more than one core

[gelisam]

One downside I see is that in order to make debugging easier, the current implementation is intentionally (1) deterministic, in the sense that whenever we could pick between many task, we always try the first one in the list, and (2) observable, in the sense that all the state is kept in one giant state object which can be printed out and examined, it's not distributed among many private fields in many concurrent threads.

Using threads seemingly breaks (1), except of course the whole point of lvish is to restore determinism in the presence of unpredictable thread scheduling.

As for (2)... I don't know. On one hand, this is the first Haskell project I'm working on which intentionally has this property, so I feel like I can manage just fine without it. On the other hand, choosing to structure the code this way was a deliberate choice by @david-christiansen, clearly one which comes from hard-won experience, so I don't feel like I'm the best person to decide whether losing this property is a cost worth paying. I can definitely remember situations in other projects when it would have been very convenient if that project had that property! Still, since determinism is such a key aspect of this particular project... I think it's probably worth it.

(Aside: this makes me want to write a Klister #lang which automatically adds all the debugging levers needed to give programs this property without requiring the program to be architected in this very restricted manner)

[gelisam]

Ouch, lvish only supports ghc-7.10? I hope it's just a needlessly-restrictive upper bound...

[gelisam]

I am working on an lvish PR for allowing it to support more modern versions of ghc. See iu-parfunc/lvars#130 for details.

[david-christiansen]

I think that, now that things are working reasonably well, it would be fine to use more higher-order stuff in the state, to use real concurrency in the expander, and so forth. When I was trying to get hygiene and phased modules to work, being able to dump the state made it much easier to work out really subtle bugs with scope sets, but I haven't seen one of them for a really long time now.

Our determinism should be guaranteed by the semantics of our language, not by the implementation being deterministic. A good test would be to randomize the order of the job queue at every iteration, and see if tests start failing.

[doyougnu]

I'd prefer to use lvish as inspiration and as a reference rather than directly using it in the project. IMHO we should have a separate implementation because we have different goals. My fear is that we'll have a maintenance burden by coupling with lvish and that we'll inherit any design decisions that were made in lvish in pursuit of its goals that no longer make sense for our goals.

Using lvish (as opposed to just mentioning it) would allow us to:

• build on lvish's proof of correctness to drastically simplify our proof effort
• it would allow us to add new builtins more confidently, because lvish will check that we are not breaking our claim.
• speed up the implementation by using more than one core

the first one is the real problem. The second is just a maintenance effect from the first, and the third is an another goal entirely, one which might require plenty of other changes. So I want to ask do we need to prove the unordered task schedule property for klister? Does that proof need to be mechanized (I'm not keen on Hasochism)? It seems perfectly reasonable to me to prove this property via the semantics of klister (in the abstract) and then have an implementation that abides by those semantics (that's this project).

good test would be to randomize the order of the job queue at every iteration, and see if tests start failing.

Exactly. We should be testing the implementation and proving based on the language not the implementation. Unless of course we implment dependant typing and then can have the implementation prove the property itself.

[gelisam]

My fear is that we'll have a maintenance burden by coupling with lvish

I'm confused. When you discovered that I had reimplemented the golden-testing logic instead of using the tasty-golden library, you said:

I'm hesitant to keep code that reimplements a commonly used library unless that library has some significant issue. Only because then we don't benefit from any future updates or features and there is no need to reinvent the wheel as long as the lib can do what we need.

What's the criterion for when using an existing library is a maintenance burden and thus we should roll our own, and when rolling our own means reinventing the wheel and robs us of future updates and features and thus we should be using an existing library?

[gelisam]

Note that this issue is about the Haskell implementation of Klister. This issue should not be confused with #168 , which is about adding an lvish-like feature to the Klister programming language. The two changes are independent, and nobody is proposing that reimplementing the task queue using lvish would be a good way to implement #168 .

[gelisam]

do we need to prove the unordered task schedule property for klister?

Nobody is twisting our arm, we can do it if we feel like it :)

Does that proof need to be mechanized [...]?

It can be formal if we feel like it!

Currently, we have a very informal argument: we were careful in the design of our primitives, so we think the property holds. But it's not a very solid claim.

If the implementation was using lvish, which is theoretically only able to express deterministic parallel computations, then we would have a stronger claim.

If we wanted to write a formal proof, I think we would need to simplify Klister down to a calculus with very few primitives, then provide single step operational semantics which allow more than one path to reach a value, and then prove confluence.

If we wanted a computer-checked proof, we could use a proof assistant to check the proof from the previous paragraph.

If we wanted to prove that the real implementation also satisfies the property, not just the calculus, then we would need to port the implementation from Haskell to a proof assistant, and we'd have to write a longer version of the proof in the previous paragraph.

Personally, I think the lvish and calculus approaches are reasonable and worthwhile, while the mechanically-checked approches are overkill.

I have never used lvish, I have never seen a calculus for macro languages, and I have never proved confluence. But I have learned many Haskell libraries before, so the lvish approach is the one which scares me the least.

It seems perfectly reasonable to me to prove this property via the semantics of klister (in the abstract) and then have an implementation that abides by those semantics (that's this project).

The calculus approach does seem reasonable, yes.

[gelisam]

good test would be to randomize the order of the job queue at every iteration, and see if tests start failing.

Exactly. We should be testing the implementation and proving based on the language not the implementation.

That's a test we've been meaning to do for a long time, one which we should implement regardless of whether or not we switch to lvish. Let's move that part of the discussion to #214.