From a776c8b1587887f75fe4065780165172e57c862c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Nov 2013 11:32:09 -0800
Subject: [PATCH] feat(util/interrupt): add sleep_for, and simplify
 request_interrupt

The Lean sleep_for checks the interrupt flag from time to time.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/bindings/lua/leanlua_state.cpp |  5 +----
 src/tests/kernel/normalizer.cpp    |  3 +--
 src/tests/kernel/type_checker.cpp  |  3 +--
 src/tests/util/thread.cpp          | 19 ++++++++++++++++++-
 src/util/interrupt.cpp             | 29 +++++++++++++++++++++++------
 src/util/interrupt.h               | 15 ++++++++++++++-
 6 files changed, 58 insertions(+), 16 deletions(-)

diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp
index 0e5caaeae..144e67e06 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/bindings/lua/leanlua_state.cpp
@@ -521,10 +521,7 @@ public:
     }
 
     void request_interrupt() {
-        while (!m_thread.request_interrupt()) {
-            check_interrupted();
-            std::this_thread::sleep_for(g_small_delay);
-        }
+        m_thread.request_interrupt();
     }
 
     void write(lua_State * src, int first, int last) {
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index 62382a4fe..01af51631 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -231,8 +231,7 @@ static void tst5() {
             }
         });
     std::this_thread::sleep_for(dura);
-    while (!thread.request_interrupt()) {
-    }
+    thread.request_interrupt();
     thread.join();
 #endif
 }
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 2b3c7ba8e..84beee6f5 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -239,8 +239,7 @@ static void tst12() {
             }
         });
     std::this_thread::sleep_for(dura);
-    while (!thread.request_interrupt()) {
-    }
+    thread.request_interrupt();
     thread.join();
 #endif
 }
diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp
index 66553518f..9fe4b9d97 100644
--- a/src/tests/util/thread.cpp
+++ b/src/tests/util/thread.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include <atomic>
 #include "util/debug.h"
 #include "util/shared_mutex.h"
+#include "util/interrupt.h"
 using namespace lean;
 
 void foo() {
@@ -124,7 +125,6 @@ static void tst4() {
     lean_assert(t2_done);
 }
 
-
 static void tst5() {
     shared_mutex      mutex;
     std::atomic<bool> t2_started(false);
@@ -158,10 +158,26 @@ static void tst5() {
     t1.join();
     t2.join();
 }
+
+static void tst6() {
+    interruptible_thread t1([]() {
+            try {
+                // Remark: std::this_thread::sleep_for does not check whether the thread has been interrupted or not.
+                // std::this_thread::sleep_for(std::chrono::milliseconds(1000000));
+                sleep_for(1000000);
+            } catch (interrupted &) {
+                std::cout << "interrupted...\n";
+            }
+        });
+    sleep_for(20);
+    t1.request_interrupt();
+    t1.join();
+}
 #else
 static void tst3() {}
 static void tst4() {}
 static void tst5() {}
+static void tst6() {}
 #endif
 
 int main() {
@@ -170,5 +186,6 @@ int main() {
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp
index d77ea6b11..a4ec2f0cc 100644
--- a/src/util/interrupt.cpp
+++ b/src/util/interrupt.cpp
@@ -29,6 +29,19 @@ void check_interrupted() {
     }
 }
 
+void sleep_for(unsigned ms, unsigned step_ms) {
+    if (step_ms == 0)
+        step_ms = 1;
+    unsigned rounds = ms / step_ms;
+    std::chrono::milliseconds c(step_ms);
+    std::chrono::milliseconds r(ms % step_ms);
+    for (unsigned i = 0; i < rounds; i++) {
+        std::this_thread::sleep_for(c);
+        check_interrupted();
+    }
+    std::this_thread::sleep_for(r);
+}
+
 std::atomic_bool * interruptible_thread::get_flag_addr() {
     return &g_interrupt;
 }
@@ -40,12 +53,16 @@ bool interruptible_thread::interrupted() const {
     return f->load();
 }
 
-bool interruptible_thread::request_interrupt() {
-    std::atomic_bool * f = m_flag_addr.load();
-    if (f == nullptr)
-        return false;
-    f->store(true);
-    return true;
+void interruptible_thread::request_interrupt(unsigned try_ms) {
+    while (true) {
+        std::atomic_bool * f = m_flag_addr.load();
+        if (f != nullptr) {
+            f->store(true);
+            return;
+        }
+        std::this_thread::sleep_for(std::chrono::milliseconds(try_ms));
+        check_interrupted();
+    }
 }
 
 void interruptible_thread::join() {
diff --git a/src/util/interrupt.h b/src/util/interrupt.h
index 79d08921c..c1f64c530 100644
--- a/src/util/interrupt.h
+++ b/src/util/interrupt.h
@@ -29,6 +29,15 @@ bool interrupt_requested();
 */
 void check_interrupted();
 
+constexpr unsigned g_small_sleep = 50;
+
+/**
+   \brief Put the current thread to sleep for \c ms milliseconds.
+
+   \remark check_interrupted is invoked every \c step_ms milliseconds;
+*/
+void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep);
+
 /**
    \brief Thread that provides a method for setting its interrupt flag.
 */
@@ -56,8 +65,12 @@ public:
     /**
        \brief Send a interrupt request to the current thread. Return
        true iff the request has been successfully performed.
+
+       \remark The main thread may have to wait the interrupt flag of this thread to
+       be initialized. If the flag was not initialized, then the main thread will be put
+       to sleep for \c try_ms milliseconds until it tries to set the flag again.
     */
-    bool request_interrupt();
+    void request_interrupt(unsigned try_ms = g_small_sleep);
 
     void join();
     bool joinable();