• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
    • Oslib
    • Bridge
      • Json-encoding
      • Security
      • Command
      • In-main-thread
      • Message
      • Start
      • Bindings
      • Stop
      • Try-in-main-thread
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bridge

In-main-thread

Special mechanism for making sure forms execute in the main thread.

This is a special form that is only meant to be used by ACL2 Bridge clients when they issue commands. A syntax example is:

(bridge::in-main-thread (memoize 'fib) (fib 37))

This is really just a hack that lets you use commands that, for one reason or another, must only ever be executed in the "main" thread (in CCL parlance, the "initial listener" thread). Practical applications include:

• Running memoized functions (the memoization code isn't thread-safe, and attempts to use a memoized function in multiple thread can result in hard errors), and
• Doing computations that involve a lot of honsing (otherwise, each thread has its own hons space, and you may not get the sharing you are expecting).

If the main thread is busy with work from other clients, this form will wait until it becomes available again. See also try-in-main-thread, which instead just causes an error if the main thread is busy.