Fix windows binaries exiting with code 24

[isanych]

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]

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]

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]

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]

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