Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typer domain #1890

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

Typer domain #1890

wants to merge 3 commits into from

Conversation

lyrm
Copy link

@lyrm lyrm commented Jan 29, 2025

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

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.

Design Notes & Expected Changes

Laziness

As noted in the Lazy module documentation:

Note: Lazy.force is not concurrency-safe. If you use this module with multiple fibers, systhreads or domains, then you will need to add some locks. The module however ensures memory-safety, and hence, concurrently accessing this module will not lead to a crash but the behavior is unspecified.

Since laziness is inherently unsafe 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.

These issues are not currently resolved.

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 the Typer Domain

Currently, concurrency is handled using atomic top-level values, which rely on active polling. This approach will likely be replaced (at least partially) with mutexes and conditions variables, allowing the domains to perform passive waiting instead.

Credits

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant