Concurrent lean

Stream: general

[Mario Carneiro]

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]

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]

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

[Gabriel Ebner]

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]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Mario Carneiro]

How is that different from task.delay?

[Gabriel Ebner]

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

[Mario Carneiro]

lol that's quite a large cardinal

[Sebastian Ullrich]

Okay, I think I fixed the signature

[Gabriel Ebner]

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]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

New results from your master thesis?

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

Does it just drop the thread?

[Mario Carneiro]

What if you call task.get twice?

[Gabriel Ebner]

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]

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]

Ooh, that sounds like memoization

[Mario Carneiro]

Maybe memoized is definable after all...

[Sebastian Ullrich]

It's what thunk should sound like :laughing:

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Gabriel Ebner]

Immediately creates a task on another thread...

[Mario Carneiro]

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

[Gabriel Ebner]

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.

[Mario Carneiro]

Oh, I see...

[Mario Carneiro]

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

[Gabriel Ebner]

Do you actually use them?

[Sebastian Ullrich]

:)

[Mario Carneiro]

I use timeit and trace all the time

[Sebastian Ullrich]

Hmm, good to know I guess

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Gabriel Ebner]

That's nondeterministic and hence unsupported by design.

[Mario Carneiro]

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

[Mario Carneiro]

I think it should probably be renamed nondet

[Sebastian Ullrich]

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]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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]

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

[Sebastian Ullrich]

@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.

[Gabriel Ebner]

Ah, I see.

[Mario Carneiro]

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]

what is unrun? That seems a bit paradoxical

[Sebastian Ullrich]

unrun has since been removed :)

[Mario Carneiro]

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

[Sebastian Ullrich]

io is non-meta now :)

[Mario Carneiro]

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

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Mario Carneiro]

is unit a monad in lean?

[Sebastian Ullrich]

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

[Mario Carneiro]

or I guess λ _, unit

[Sebastian Ullrich]

There's also https://github.com/leanprover/lean/blob/efa9d7e110ff6389e8863551a4882c84dbcf8236/tests/lean/run/rebind_bind.lean

[Mario Carneiro]

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

[Sebastian Ullrich]

Yep, that's the main purpose of the test

[Kevin Buzzard]

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

[Mario Carneiro]

Check it out:

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

#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]

too bad it has to be meta

[Adam Kurkiewicz]

impressive! What keeps it in meta?