Opened 9 months ago

Closed 8 months ago

#21 closed feature (fixed)

Implement clock_gettime

Reported by: John Lång Owned by: mornfall
Priority: minor Milestone: 4.2
Component: DiOS Keywords: clock, time, date
Cc:

Description

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.

Change History (4)

comment:1 Changed 9 months ago by 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.

comment:2 Changed 9 months ago by John Lång

Summary: Request for Implementing clock_gettimeImplement clock_gettime

comment:3 Changed 9 months ago by mornfall

Component: benchDiOS
Status: newaccepted

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).

comment:4 Changed 8 months ago by mornfall

Milestone: future4.2
Resolution: fixed
Status: acceptedclosed

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.

Note: See TracTickets for help on using tickets.