JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
584 stars 34 forks source link

Improve support of time-related APIs in the model checking mode #390

Open eupp opened 1 month ago

eupp commented 1 month ago

Currently, Lincheck provides a naive implementation of time APIs in the model checking mode (some predefined constant is always returned). In order to support more complex code relying on timing (e.g. relying on delay), we need a more precise model of time APIs.

eupp commented 1 month ago

To better understand how to model time in the model checking mode it would be very helpful to first collect some concrete examples of the code we want to test (e.g. from kotlinx-coroutines).