From b31233e8c29451813c423a109b6e421f3e884afb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Nov 2013 21:16:10 -0800
Subject: [PATCH] feat(util/interrupt): restore interrupt module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/CMakeLists.txt |  4 +--
 src/util/interrupt.cpp  | 56 +++++++++++++++++++++++++++++++++++
 src/util/interrupt.h    | 65 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 123 insertions(+), 2 deletions(-)
 create mode 100644 src/util/interrupt.cpp
 create mode 100644 src/util/interrupt.h

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 5f43c10aa..6f6fcb2c1 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
-  hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp
-  memory.cpp shared_mutex.cpp)
+  interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp
+  ascii.cpp memory.cpp shared_mutex.cpp)
diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp
new file mode 100644
index 000000000..98a655cac
--- /dev/null
+++ b/src/util/interrupt.cpp
@@ -0,0 +1,56 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/interrupt.h"
+#include "util/exception.h"
+
+namespace lean {
+static thread_local std::atomic_bool g_interrupt;
+
+void request_interrupt() {
+    g_interrupt.store(true);
+}
+
+void reset_interrupt() {
+    g_interrupt.store(false);
+}
+
+bool interrupted() {
+    return g_interrupt.load();
+}
+
+void check_interrupt() {
+    if (interrupted())
+        throw interrupted();
+}
+
+std::atomic_bool * interruptible_thread::get_flag_addr() {
+    return &g_interrupt;
+}
+
+bool interruptible_thread::interrupted() const {
+    std::atomic_bool * f = m_flag_addr.load();
+    if (f == nullptr)
+        return false;
+    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::join() {
+    m_thread.join();
+}
+
+bool interruptible_thread::joinable() {
+    return m_thread.joinable();
+}
+}
diff --git a/src/util/interrupt.h b/src/util/interrupt.h
new file mode 100644
index 000000000..7f9cddb1e
--- /dev/null
+++ b/src/util/interrupt.h
@@ -0,0 +1,65 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <atomic>
+#include <thread>
+#include <utility>
+
+namespace lean {
+/**
+   \brief Mark flag for interrupting current thread.
+*/
+void request_interrupt();
+/**
+   \brief Reset (interrupt) flag for current thread.
+*/
+void reset_interrupt();
+
+/**
+   \brief Return true iff the current thread was marked for interruption.
+*/
+bool interrupted();
+
+/**
+   \brief Throw an interrupt exception if the (interrupt) flag is set.
+*/
+void check_interrupt();
+
+/**
+   \brief Thread that provides a method for setting its interrupt flag.
+*/
+class interruptible_thread {
+    std::atomic<std::atomic_bool*> m_flag_addr;
+    std::thread                    m_thread;
+    static std::atomic_bool *      get_flag_addr();
+public:
+    template<typename Function, typename... Args>
+    interruptible_thread(Function && fun, Args &&... args):
+        m_flag_addr(nullptr),
+        m_thread(
+            [&](Function&& fun, Args&&... args) {
+                m_flag_addr.store(get_flag_addr());
+                fun(std::forward<Args>(args)...);
+            },
+            std::forward<Function>(fun),
+            std::forward<Args>(args)...)
+        {}
+
+    /**
+       \brief Return true iff an interrupt request has been made to the current thread.
+    */
+    bool interrupted() const;
+    /**
+       \brief Send a interrupt request to the current thread. Return
+       true iff the request has been successfully performed.
+    */
+    bool request_interrupt();
+
+    void join();
+    bool joinable();
+};
+}