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 YICESMODE=debug revealed a number of places where the MC-SAT code was calling yices API functions (which take the global lock) rather than _oyices 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 74f5f3b0689976535883061e9ab3ea9dca28844d on markpmitchell:mcsat-thread-safety into 6903281942d9ea67f09a1dd493167ce2bc466b87 on SRI-CSL:master.

[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 https://github.com/SRI-CSL/yices2/pull/456#discussion_r1334630099:

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 https://github.com/SRI-CSL/yices2/pull/456#pullrequestreview-1640348754, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVS3GHJ7RRD5IWI3CIV4TX3W77NANCNFSM6AAAAAA5CLVCBM. You are receiving this because you authored the thread.

[ahmed-irfan]

I understand.