Zulip Chat Archive

Stream: general

Topic: Concurrent lean


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 07:47):

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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 07:48):

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

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 07:48):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:48):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:48):

How is that different from task.delay?

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 07:49):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:49):

lol that's quite a large cardinal

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 07:51):

Okay, I think I fixed the signature

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:52):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 07:54):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:56):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:57):

Does it just drop the thread?

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:57):

What if you call task.get twice?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 28 2018 at 07:59):

Ooh, that sounds like memoization

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:00):

Maybe memoized is definable after all...

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:00):

It's what thunk should sound like :laughing:

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:01):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:02):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:03):

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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 08:03):

Immediately creates a task on another thread...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:06):

Oh, I see...

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 08:08):

Do you actually use them?

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:08):

:)

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:08):

I use timeit and trace all the time

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:09):

Hmm, good to know I guess

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:10):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 08:12):

That's nondeterministic and hence unsupported by design.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:13):

I think it should probably be renamed nondet

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:17):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 08:24):

Ah, I see.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:26):

what is unrun? That seems a bit paradoxical

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:27):

unrun has since been removed :)

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:30):

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

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:30):

io is non-meta now :)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:37):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:38):

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

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:39):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:43):

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

view this post on Zulip Gabriel Ebner (Mar 28 2018 at 08:44):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:45):

is unit a monad in lean?

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:46):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:46):

or I guess λ _, unit

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:47):

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

view this post on Zulip Mario Carneiro (Mar 28 2018 at 08:48):

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

view this post on Zulip Sebastian Ullrich (Mar 28 2018 at 08:49):

Yep, that's the main purpose of the test

view this post on Zulip Kevin Buzzard (Mar 28 2018 at 10:20):

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

view this post on Zulip 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
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

view this post on Zulip Mario Carneiro (Mar 30 2018 at 07:06):

too bad it has to be meta

view this post on Zulip Adam Kurkiewicz (Mar 30 2018 at 12:51):

impressive! What keeps it in meta?


Last updated: May 13 2021 at 06:15 UTC