## Stream: general

### Topic: Concurrent lean

#### Mario Carneiro (Mar 28 2018 at 01:54):

I've been thinking about what appropriate concurrency primitives can be used in pure lean. @Gabriel Ebner Do you see any problems with modeling task in lean (being the same as thunk)? It's not clear why this needs to be meta.

Another possible concurrency primitive is fork : thunk A -> thunk B -> A x B which runs the two thunks on separate threads and then returns the results. There is an obvious generalization here to peval : list (thunk A) -> list A, not sure if this is better or worse than join as a primitive. I'm not sure how to simulate these forking strategies with task.

#### Mario Carneiro (Mar 28 2018 at 01:56):

I hoped to get inspiration from ML and Haskell, but ML is too declarative (unit functions everywhere) and Haskell has funny problems with laziness turning the evaluation order inside out. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parallel_haskell2.pdf

#### Sebastian Ullrich (Mar 28 2018 at 07:41):

fork f g = let tf = task.delay t in let tg = task.delay g in (tf.get, tg.get)?

#### Gabriel Ebner (Mar 28 2018 at 07:43):

task is perfectly sound, and does not need to be meta. A possible model for task is id, and you should not be able to observe any differences from id in pure Lean code.

#### Sebastian Ullrich (Mar 28 2018 at 07:44):

Or less resource-hungry, fork f g = let tf = task.delay f in let y = g () in (tf.get, y)

#### Mario Carneiro (Mar 28 2018 at 07:47):

Isn't the evaluation semantics off from id though? You need thunk to avoid evaluating the argument too soon

#### Gabriel Ebner (Mar 28 2018 at 07:47):

That's why I said pure Lean code. :smile:

#### Gabriel Ebner (Mar 28 2018 at 07:48):

Of course, task hides nontermination and C++ exceptions.

#### Sebastian Ullrich (Mar 28 2018 at 07:48):

One missing ingredient right now is task.delay_io : {α : Type u} (f : io α) : io (task α)

#### Mario Carneiro (Mar 28 2018 at 07:48):

Neither can happen in non-meta code though, right?

#### Mario Carneiro (Mar 28 2018 at 07:48):

How is that different from task.delay?

#### Gabriel Ebner (Mar 28 2018 at 07:49):

You can have nontermination without meta if you add axiom large_cardinal : 0 = 1

#### Mario Carneiro (Mar 28 2018 at 07:49):

lol that's quite a large cardinal

#### Sebastian Ullrich (Mar 28 2018 at 07:51):

Okay, I think I fixed the signature

#### Gabriel Ebner (Mar 28 2018 at 07:51):

Right now, there is also the slight performance problem that we serialize the thunk passed to task.delay, and then deserialize it on the thread where it executes. From the last public state of the Lean 4 design document, this should be solved in Lean 4.

#### Mario Carneiro (Mar 28 2018 at 07:51):

Well, you can break the VM in many ways using large_cardinal, you don't need task

#### Mario Carneiro (Mar 28 2018 at 07:52):

in fact you should be able to get nontermination even without task

#### Gabriel Ebner (Mar 28 2018 at 07:52):

in fact you should be able to get nontermination even without task

New results from your master thesis?

#### Mario Carneiro (Mar 28 2018 at 07:53):

No, maybe it's folklore... But you can just evaluate a false proof of well_founded in the VM

#### Gabriel Ebner (Mar 28 2018 at 07:54):

Ok, that's essentially the same thing as large_cardinal, or sorry.

#### Mario Carneiro (Mar 28 2018 at 07:54):

right, that's my point - from a false axiom you can fake a wf definition to cause nontermination

#### Mario Carneiro (Mar 28 2018 at 07:55):

(in the VM, which doesn't do reduction and so doesn't get stuck like #reduce would)

#### Mario Carneiro (Mar 28 2018 at 07:56):

What is the behavior of let f := task.delay f in ()?

#### Mario Carneiro (Mar 28 2018 at 07:57):

Does it just drop the thread?

#### Mario Carneiro (Mar 28 2018 at 07:57):

What if you call task.get twice?

#### Gabriel Ebner (Mar 28 2018 at 07:58):

What is the behavior of let f := task.delay f in ()?

f continues to execute, you can continue printing trace messages, etc., and they will show up.

#### Gabriel Ebner (Mar 28 2018 at 07:59):

What if you call task.get twice?

The first time you call task.get, it will wait for the task to finish and return the result. The second time it will return immediately with the result. The code in the task is only executed once.

#### Mario Carneiro (Mar 28 2018 at 07:59):

Ooh, that sounds like memoization

#### Mario Carneiro (Mar 28 2018 at 08:00):

Maybe memoized is definable after all...

#### Sebastian Ullrich (Mar 28 2018 at 08:00):

It's what thunk should sound like :laughing:

#### Mario Carneiro (Mar 28 2018 at 08:01):

I think Leo said something about explicitly wanting thunk to not be memoized, although I think it's a poor name if that's the intent

#### Gabriel Ebner (Mar 28 2018 at 08:01):

It's like memoization except that the code starts running immediately, and on another thread. C++ code has the ability to create tasks that do not start immediately though (in fact, that's even the default behavior).

#### Sebastian Ullrich (Mar 28 2018 at 08:01):

Btw, we will most probably move those horrible impure init.util functions into io

#### Mario Carneiro (Mar 28 2018 at 08:02):

You can create delayed tasks with thunk (task A) I guess

#### Gabriel Ebner (Mar 28 2018 at 08:02):

This will create a new task every time you evaluate the thunk, probably not what you want.

#### Mario Carneiro (Mar 28 2018 at 08:03):

hm... task (task A)? :)

#### Mario Carneiro (Mar 28 2018 at 08:04):

but I guess if the real work is in the created task that won't be executed until you flatten

#### Gabriel Ebner (Mar 28 2018 at 08:05):

If you do task.delay (task.delay ()), you first create task A, which immediately begins executing on thread 2. This task A then creates task B, which again immediately begins executing () on thread 3.

Oh, I see...

#### Mario Carneiro (Mar 28 2018 at 08:08):

@Sebastian Ullrich I really like those non-io functions. As long as they are observationally pure there is no problem

#### Gabriel Ebner (Mar 28 2018 at 08:08):

Do you actually use them?

:)

#### Mario Carneiro (Mar 28 2018 at 08:08):

I use timeit and trace all the time

#### Sebastian Ullrich (Mar 28 2018 at 08:09):

Hmm, good to know I guess

#### Mario Carneiro (Mar 28 2018 at 08:10):

Actually I've never used io in pure code. It seems like a trap

#### Gabriel Ebner (Mar 28 2018 at 08:10):

I just realized that you can't even simulate them via unsafe_perform_io, since that is meta.

#### Mario Carneiro (Mar 28 2018 at 08:12):

Here's another missing task primitive: Run f g : thunk A, and return the first one that finishes

#### Gabriel Ebner (Mar 28 2018 at 08:12):

That's nondeterministic and hence unsupported by design.

#### Mario Carneiro (Mar 28 2018 at 08:12):

The obvious problem is that they might not return the same thing, but cached solves that problem handily

#### Mario Carneiro (Mar 28 2018 at 08:13):

I think it should probably be renamed nondet

#### Sebastian Ullrich (Mar 28 2018 at 08:13):

Did you see my beautiful typeclass for lifting these functions in the extended monad PR? Fortunately I found a more general monad class that subsumes it https://github.com/Kha/lean/commit/974fee78f75c8861477fba9143a49c8e08101b41#diff-f8e23e5e864df768277396e6f07b2809L67

#### Gabriel Ebner (Mar 28 2018 at 08:14):

@Sebastian Ullrich This does not help you if you want to do printf-style debugging in a pure non-monadic function, right?

#### Sebastian Ullrich (Mar 28 2018 at 08:16):

Then you don't need any lifting, no? This is still with the current pure definition instead of in io.

#### Mario Carneiro (Mar 28 2018 at 08:17):

Is there a @[noinline] or @[volatile] attribute for these functions?

#### Gabriel Ebner (Mar 28 2018 at 08:17):

Right. You proposed the lifting functions as a replacement for the pure ones, that's what I was responding to.

#### Mario Carneiro (Mar 28 2018 at 08:20):

Alternatively, you could accept a proof f () = g () to eliminate the nondeterminism. This is roughly equivalent to the cached approach without boxing up the result

#### Mario Carneiro (Mar 28 2018 at 08:21):

(This is not an unreasonable constraint, if it's not true you can just quotient the output type to make it true)

#### Sebastian Ullrich (Mar 28 2018 at 08:23):

@Gabriel Ebner No, that was intended for correctly lifting "pure" scoping functions thunk A -> A into thunk (state S A) -> state S A, etc. But the same approach would be used for lifting io A -> io A scoping functions, yes. The good thing is that with the latter, you can't accidentally forget the lift. Which is the main reason why I think the current definitions are pretty evil.

Ah, I see.

#### Mario Carneiro (Mar 28 2018 at 08:25):

I think that using scoping functions to build an io computation is certainly bad practice; the trace output should be expected to be nondeterministic

#### Mario Carneiro (Mar 28 2018 at 08:26):

what is unrun? That seems a bit paradoxical

#### Sebastian Ullrich (Mar 28 2018 at 08:27):

unrun has since been removed :)

#### Mario Carneiro (Mar 28 2018 at 08:30):

Now that io_interface is gone, is it impossible to non-meta write io programs?

#### Sebastian Ullrich (Mar 28 2018 at 08:30):

io is non-meta now :)

#### Mario Carneiro (Mar 28 2018 at 08:31):

yeah, but not really, it relies on a meta constant that is not actually meta for some reason

#### Sebastian Ullrich (Mar 28 2018 at 08:34):

I think the idea was to not force users to annotate all io functions with meta. You can't prove anything about it, but it's still sound. The replacement for io_interface is monad_io.

#### Mario Carneiro (Mar 28 2018 at 08:34):

Oh, I guess the idea is you should replace io_core with your own implementation of monad_io_terminal etc

#### Mario Carneiro (Mar 28 2018 at 08:37):

How do you know it's sound? Writing an implementation is not trivial, I think

#### Mario Carneiro (Mar 28 2018 at 08:38):

in particular there is a constructor that gives unbounded recursion in the monad

#### Sebastian Ullrich (Mar 28 2018 at 08:39):

Which should be okay as long as there's no eliminator, no?

#### Mario Carneiro (Mar 28 2018 at 08:42):

hm, I guess you can do some kind of coinductive trace thing if you don't want to have it be trivial

#### Mario Carneiro (Mar 28 2018 at 08:43):

Oh cool I just noticed we have a random number generator in lean now

#### Gabriel Ebner (Mar 28 2018 at 08:44):

For soundness it should be enough to set io_core := λ _ _, unit.

#### Mario Carneiro (Mar 28 2018 at 08:45):

is unit a monad in lean?

#### Sebastian Ullrich (Mar 28 2018 at 08:46):

It's not even a type constructor...?

#### Mario Carneiro (Mar 28 2018 at 08:46):

or I guess λ _, unit

#### Mario Carneiro (Mar 28 2018 at 08:48):

interesting. You are using do notation with something that's not monad.bind?

#### Sebastian Ullrich (Mar 28 2018 at 08:49):

Yep, that's the main purpose of the test

#### Kevin Buzzard (Mar 28 2018 at 10:20):

mono_monad? Reminds me of https://www.youtube.com/watch?v=8N_tupPBtWQ

#### Mario Carneiro (Mar 30 2018 at 07:05):

Check it out:

meta def list.par_map {α β} (f : α → β) (l : list α) : list β :=
let fs := l.map (λ a, task.delay (λ _, f a)) in

#eval timeit "" ((list.range' 50000 10).map (λ n, (eratosthenes n).length))
-- 6.87s
#eval timeit "" ((list.range' 50000 10).par_map (λ n, (eratosthenes n).length))
-- 2.78s


#### Mario Carneiro (Mar 30 2018 at 07:06):

too bad it has to be meta

#### Adam Kurkiewicz (Mar 30 2018 at 12:51):

impressive! What keeps it in meta?

Last updated: May 13 2021 at 06:15 UTC