search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
363 stars 45 forks source link

Improve thread-safety #457

Closed markpmitchell closed 10 months ago

markpmitchell commented 10 months ago
  1. Eliminate yices_smt2_mt frontend, incorporating multi-thread test functionality into yices_smt2.
  2. Provide a thread-safe implementation of timeouts.
  3. Avoid allocating very large arrays on the stack. (Noticed because it caused threads, which have smaller stacks, to crash.) Variable-sized allocation on the stack is a bad idea if the allocation size is not bounded.
  4. For testing purposes, give thread stacks the same size as the main stack. (Necessary to work around the fact that libcudd uses recursion where it should use iteration in at least one place.)
  5. Enhance check.sh to allow passing additional options to tests and to allow running individual tests.
  6. Clean up error-handling for POSIX threads API.
  7. Fix incorrect order of destruction in yices_exit.

With these changes, all regression tests pass with --enable-mcsat --enable-thread-safety when running the yices_smt2 frontend with 8 threads.

coveralls commented 10 months ago

Coverage Status

coverage: 64.976% (+0.003%) from 64.973% when pulling 88e46491182753b7023c87e4de55bc821f3be9ba on markpmitchell:mcsat-thread-safety into 618cbb3b5ea3511850e308be25a23be797c0523d on SRI-CSL:master.

disteph commented 10 months ago

Looks good, thanks!