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

Fix windows binaries exiting with code 24 #449

Open isanych opened 1 year ago

isanych commented 1 year ago

Unfortunately I cannot provide reasonable reproducible example - but we had regular cases when binary sporadically exit with code 24 on big multithreaded projects on windows only, when linux binary working fine on the same project on similar hardware. Looks like windows code intended to be initialized differently vs posix, but as posix code is working and compatible with windows we have not looked into details too much. With this change our windows binaries are working as expected, without issues seen before.

markpmitchell commented 9 months ago

Is yices_init being called in multiple threads? If so, how many? Is yices_exit being called before yices_init is being called again? The Windows code would seem to exit with code 24 if there are no more TLS indices -- and there should be plenty.

wojbas commented 9 months ago

The Win32 code is wrong in that the TLS should be initialized once (in yices_init), not per thread (as is the case now in yices_per_thread_init), so consumes a slot with every call to yices_per_thread_init, which we call a lot.

markpmitchell commented 9 months ago

I’m guessing, from the reference to yices_per_thread_init, that this is on the per-thread-state branch, then?

— Mark Mitchell

On Oct 17, 2023, at 11:53 PM, Wojtek Basalaj @.***> wrote:

@wojbas commented on this pull request.

In src/api/yices_error_report_win.c https://github.com/SRI-CSL/yices2/pull/449#discussion_r1363340775:

-static void thread_local_free_yices_error_report(void){

  • error_report_t* tl_yices_error = TlsGetValue(yices_tls_error_index);
  • safe_free(tl_yices_error);
  • TlsSetValue(yices_tls_error_index, NULL); -}

  • -void init_yices_error(void){

  • /*
    • This is called explicitly in yices_init, so if there is a race
    • condition here, then there is a race condition b/w yices_init and
    • a call to the API. Which is not OUR problem. Just incorrect
    • usage of the API.
  • */
  • if (!yices_tls_initialized) {
  • yices_tls_error_index = TlsAlloc(); despite the comment above this is called via yices_per_thread_init and not yices_init

— Reply to this email directly, view it on GitHub https://github.com/SRI-CSL/yices2/pull/449#pullrequestreview-1684228546, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVS3FPBK7TLPTF3QR4RSLX754IHAVCNFSM6AAAAAAZ6VM6SWVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTMOBUGIZDQNJUGY. You are receiving this because you commented.

isanych commented 9 months ago

yep, it is PR for per-thread-state branch