Lwt.pause needs to be used three times

[madroach]

Hi,

I'm working with a ssl connection. A reader is permanently watching it for data or EOF.
After few seconds of calculations this ssl connection might have been shutdown by the remote end and an EOF is waiting to be read. Now I need to force Lwt to select so the reader can reopen the connection before writing to the already half-closed connection.

I need to call Lwt.pause three times to enforce this:

        Lwt.pause () >>= fun () ->
        Lwt.pause () >>= fun () ->
        Lwt.pause () >>= fun () ->

I added traces to the Lwt_main.run mainloop:

Lwt.pause
Lwt_main.run: after Lwt_engine.iter
Lwt.pause
Lwt_main.run: calling leave_hooks
Lwt_main.run: restart run_loop
Lwt.pause
Lwt_main.run: enter_iter_hooks
Lwt_main.run: should_block_waiting_for_io is false
Lwt_engine: after select calling readables
Lwt_ssl.read_bytes: trying to read from SSL

Is this meant to work this way? Maybe this should be documented? How am I supposed to force polling of a socket for reads before writing to it?

[raphael-proust]

Hello,

I think that Lwt_unix.sleep 0. might be a better fit for what you are looking for. (Or possibly, but I don't think you need it, Lwt_unix.sleep Float.(succ zero)?)

Lwt.pause is about cooperating with other promises rather than cooperating with the OS. Whereas Lwt_unix.sleep is the other way around. That's a wishy-washy way of explaining it. I think the issue lies with the lack of documentation of the main loop (Lwt_main.run).

[madroach]

The problem is, I cannot call into Lwt_unix, only core Lwt.

Also the documentation says:

In case your callback is just using the CPU for a really long time, you can insert a few calls to Lwt.pause into it, and resume your computation in callbacks of pause. This is basically the same as Lwt_unix.sleep0. – it's a promise that will be resolved by Lwt_main.run after any other I/O resolutions that are already in its queue.

Lwt.pause () creates a pending promise that is fulfilled after Lwt finishes calling all currently ready callbacks, i.e. it is fulfilled on the next “tick.”
Putting the rest of your computation into a callback of Lwt.pause () creates a “yield” that gives other callbacks a chance to run first.

So Lwt.pause is supposed to do the trick. And it does! It just needs to be called 3 times. Look at the trace I posted and read Lwt_main.run. paused promises are resolved twice in the mainloop. Why? Still, Lwt_unix.yield are resolved only once.

So why are pause promisis resolved so frequently. Shouldn't they be resolved only after poll/select had a chance?