Typer domain

[lyrm]

Purposes

This PR is a first draft to experiment with a typer domain, i.e., a dedicated domain that performs typing computations (partially) in parallel with the main domain, which manages the server and analyzes the results. The final implementation should also support:

• Partial typing: The typer domain provides a partial typing result to the main domain, then completes the computation.
• Interruption handling: The main domain can stop the typer when a new request invalidates the previous one

Merlin mock up to test design

The design implements here is first tried here .

Todo

There is currently a bug where tests can never finished when an exception is passed from the typer domain to the main domain. Also the reason is still unclear to me, I think part of the issue is because I use 2 different atomic to communicate between the main domain and the typer domain :

• message used during typing for cancellation and to to pass the result lock to the main domain for analysis
• close used in the highest-level loop to pass exception from the typer to the main domain and when closing merlin.

Current Changes

For now, this PR introduces the following modifications:

• Removal of laziness, which is incompatible with concurrency.
• Extension of theLocal_store scope to support computations in both domains.
• Spawning of a typer domain to execute typing concurrently.
• Moving the computation of the pipeline inside New_commands.run to be able to determine if the typer can return a partial result depending on the command.

Design Notes & Expected Changes

Laziness

Since laziness is inherently unsafe (see Lazy module documentation:) in a multicore context, it has been removed. However, this introduces new bugs as some previously deferred computations now run eagerly:

• The local_store scope must be carefully extended.
• At least one exception is currently not properly caught.

Also a type 'a lazy can't be replaced by unit -> 'a because in some cases, the typer result is used twice and without caches, it is useful as some times, some lazy values are never forced. But with caches and a cancellation mechanism it seems okay to actually always compute as much as possible.

The issue with the uncaught exception can be managed by moving the computation of the pipeline as far as possible in the code (i.e. New_commands.run) to ensure if an exception is caught by the typer domain and passed to the main domain, the main domain is always protected under a try .. with . This needs to be checked

Local Store Management

Most computation must take place when the local_store is bound. Previously, all computations were enclosed within Local_store.with_store (via Mocaml.with_state). However, this approach is not compatible with computations involving two domains.

To address this, with_store has been replaced with open_store and close_store, allowing more flexible management of the store’s scope.

This design is likely to evolve further, particularly to enable proper interruption of the typer when needed.

Concurrency with a Typer

The shared values are currently protected under mutex, or are atomic values depending on if a passive or active wait is prefered.

Todo

Currently the critical section are quite extended, especially in Mpipeline.typer_domain and Mpipeline.get where the whole loops are under mutex. The protect should be moved inside the loop, before the read of the protected value. This should not change a lot of thing but it should simplify reasoning and the risk of creating deadlocks.

Credits

This preliminary work was done with @voodoos and @xvw.