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 mingw timeout error #461

Closed ahmed-irfan closed 9 months ago

ahmed-irfan commented 9 months ago
coveralls commented 9 months ago

Coverage Status

coverage: 65.098%. remained the same when pulling a72f3a42f6e1ad6d57e7e4806b7fb7b27d4fcb7e on fix-timeout-mingw into ef6ccf72daebd114807733d3758cdb400c6c5994 on master.

markpmitchell commented 9 months ago

I missed the MinGW case in this code. Sorry!

I don't think using the_timeout makes sense on MinGW if thread-safe. When not thread-safe, the_timeout works -- but it's inherently wrong to use it when threaded. (We could put it in thread-local storage, but there's no reason that creation of a timeout and use of a timeout have to happen in the same thread.) IIUC, your patch would define the_timeout even when THREAD_SAFE is defined, which I think is a mistake.

So, I think the first hunk of the patch is correct (avoid the pthread stuff on MinGW), but the second hunk shouldn't be necessary. Right now, we don't have a thread-safe version of timeouts for MinGW, so we should add:

#if defined(THREAD_SAFE) && defined(MINGW)
#error "No thread-safe implementation of timeouts"
#endif

Does that make sense?

ahmed-irfan commented 9 months ago

So, I think the first hunk of the patch is correct (avoid the pthread stuff on MinGW), but the second hunk shouldn't be necessary. Right now, we don't have a thread-safe version of timeouts for MinGW, so we should add:

#if defined(THREAD_SAFE) && defined(MINGW)
#error "No thread-safe implementation of timeouts"
#endif

This will make the compilation of yices fail under MinGW when using THREAD_SAFE. However, we have external users who use THREAD_SAFE Yices under windows. I don't know if that should have been allowed at the first place. Do you see another way to fix the issue?

markpmitchell commented 9 months ago

The answer to "should it have been allowed?" depends on how dogmatic we want to be. No platform was actually thread-safe when using timeouts; the timeouts weren't per-thread. But, since we have Windows users relying on THREAD_SAFE, then, IMO, we should fix thread-safe timeouts to work on Windows. I'm happy to do that, if you like -- though I need to figure out how to get access to a Windows box.

In the meantime, we could define the_timeout if !defined(THREAD_SAFE) || defined(MINGW). We shouldn't define it when THREAD_SAFE when POSIX threads because the variable is never used -- and should not be used -- in that case.

ahmed-irfan commented 9 months ago

The answer to "should it have been allowed?" depends on how dogmatic we want to be. No platform was actually thread-safe when using timeouts; the timeouts weren't per-thread. But, since we have Windows users relying on THREAD_SAFE, then, IMO, we should fix thread-safe timeouts to work on Windows. I'm happy to do that, if you like -- though I need to figure out how to get access to a Windows box.

In the meantime, we could define the_timeout if !defined(THREAD_SAFE) || defined(MINGW). We shouldn't define it when THREAD_SAFE when POSIX threads because the variable is never used -- and should not be used -- in that case.

I updated the code with your suggestion. Thanks!

I will email you about the access to the windows machine that I am using.

markpmitchell commented 9 months ago

Looks good!