MC-SAT Thread Safety

[markpmitchell]

This pull request contains two components (each in its own commit):

1. Someone had tried to add debug code to detect deadlocks where a thread requests a lock that it already has. However, (a) that code was incorrectly conditionalized, meaning that it was never used, even with YICES_MODE=debug, and (b) the code was incorrect because it failed to initialize the POSIX mutex attribute. Fixed.
2. Running the test suite with YICES_MODE=debug with YICES_MODE=debug revealed a number of places where the MC-SAT code was calling yices_* API functions (which take the global lock) rather than o_yices* functions (which do not). Since the MC-SAT code is only reachable via the yices_* API, the global lock is already held at that point; there is no reason to take it again.

With these changes, the test suite passes using --enable-mcsat --enable-thread-safety. Of course, the testsuite doesn't exercise the multi-threaded mode and we have no way to prove that MC-SAT is 100% thread-safe. But, this would seem to be a step forward.

[coveralls]

coverage: 64.973% (-0.01%) from 64.983% when pulling 74f5f3b on markpmitchell:mcsat-thread-safety into 6903281 on SRI-CSL:master.

[ahmed-irfan]

minor style thing:
can we #ifdef DEBUG?

[markpmitchell]

No, we cannot — because DEBUG is never defined. :-) Of course, we could define it somewhere, but NDEBUG is the standard macro used to disable assert. And, most of the Yices code base seems to use “#ifndef NDEBUG” to guard other debug code. Thank you,

…

-- Mark Mitchell

On Sep 22, 2023, at 10:01 AM, Ahmed ***@***.***> wrote: @ahmed-irfan commented on this pull request. In src/mt/yices_locks_posix.c <#456 (comment)>: > int32_t create_yices_lock(yices_lock_t* lock){ int32_t retcode; -#ifdef DEBUG - retcode = pthread_mutexattr_settype(&mta, PTHREAD_MUTEX_ERRORCHECK); - if(retcode){ - fprintf(stderr, "create_yices_lock failed: pthread_mutexattr_settype returned %d\n", retcode); - } +#ifndef NDEBUG minor style thing: can we #ifdef DEBUG? — Reply to this email directly, view it on GitHub <#456 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKVS3GHJ7RRD5IWI3CIV4TX3W77NANCNFSM6AAAAAA5CLVCBM>. You are receiving this because you authored the thread.

[ahmed-irfan]

I understand.

[ahmed-irfan]

LGTM