Implement clock_gettime

[John Lång]

I'm trying to verify the implementation of my C++14 software framework. My project would benefit from being able to use:

• std::time
• std::localtime
• std::strftime
• std::condition_variable::wait_for

defined in <ctime> and <condition_variable>. Also, <chrono> would be useful for me. I keep getting this linkage error "Unresolved symbol (function): clock_gettime" if I try to use clock-related functionality, or the runtime error "FATAL: not implemented in userspace".

I understand that DIVINE has to be able to deliver repeatable results, so maybe these clock-related functions could be implemented with respect to a simulated system clock that would always start from a fixed, or maybe parameterized date. I understand if this feature request is not feasible to fullfill.

[John Lång]

I thank you for this great tool of DIVINE and have no hard feelings if you decide not to deliver this feature. You seem to have quite many things to do already.

[mornfall]

Both strftime and (I think) localtime should already be supported. At least for strftime, we have a testcase on the book. Actual clocks are not yet implemented (other than fixed-value stubs for some of those), but I have a plan. I'll try to land some clock support in the near future (say within a week).

[mornfall]

I have committed clock_gettime and a few related functions, should be in ​https://divine.fi.muni.cz/next now (and in /current tomorrow, or in a few days at most). We also have an implementation of pthread_cond_timedwait which is (I believe) used as the backend for std::condition_variable::wait_for. On the flip side, this timedwait function does not interact with the actual clock that I implemented today. Same is true of sleep() and related functions. Most of those issues may lead to spurious counter-examples, please do report if you encounter any.

Finally, the clock only operates in 1-second increments (micro/nanosecond fields are set to 0 and/or ignored). The default implementation of the clock just stands still (returns a constant). You can use 'verify -o clock-type:ndet' to make the clock tick non-deterministically (it will never skip a second though). This means some genuine errors may escape detection. We will try to implement symbolic clocks eventually, but those are much more tricky because our support for symbolic values is not very mature yet, and this will require some changes in that. Don't hold your breath.