lean2/src/util/thread_script_state.cpp

/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#include <vector>
#include <utility>
#include <string>
#include <memory>
#include <iostream>
#include "util/thread.h"
#include "util/pair.h"
#include "util/script_state.h"

namespace lean {
struct script_state_manager {
    static bool                          g_alive;
    mutex                                m_code_mutex;
    std::vector<pair<bool, std::string>> m_code;
    mutex                                m_state_mutex;
    std::vector<script_state>            m_states;
    std::vector<script_state>            m_available_states;
    script_state_manager() { g_alive = true; }
    ~script_state_manager() { g_alive = false; }
    static bool is_alive() { return g_alive; }
};

script_state_manager & get_script_state_manager() {
    static script_state_manager m;
    return m;
}

// make sure it is initialize at startup.
static script_state_manager & g_aux = get_script_state_manager();
bool script_state_manager::g_alive  = true;

/** \brief Execute \c code in all states in the pool */
void system_dostring(char const * code) {
    script_state_manager & m = get_script_state_manager();
    {
        // Execute code in all existing states
        lock_guard<mutex> lk(m.m_state_mutex);
        for (auto & s : m.m_states) {
            s.dostring(code);
        }
    }
    {
        // Save code for future states
        lock_guard<mutex> lk(m.m_code_mutex);
        m.m_code.push_back(mk_pair(true, code));
    }
}

/** \brief Import \c fname in all states in the pool */
void system_import(char const * fname) {
    script_state_manager & m = get_script_state_manager();
    {
        // Import file in all existing states
        lock_guard<mutex> lk(m.m_state_mutex);
        for (auto & s : m.m_states) {
            s.import_explicit(fname);
        }
    }
    {
        // Save module for future states
        lock_guard<mutex> lk(m.m_code_mutex);
        m.m_code.push_back(mk_pair(false, fname));
    }
}

static script_state get_state() {
    script_state_manager & m = get_script_state_manager();
    {
        // Try to reuse existing state
        lock_guard<mutex> lk(m.m_state_mutex);
        if (!m.m_available_states.empty()) {
            script_state r(m.m_available_states.back());
            m.m_available_states.pop_back();
            return r;
        }
    }

    {
        // Execute existing code in new state
        lock_guard<mutex> lk(m.m_code_mutex);
        script_state r;
        for (auto const & p : m.m_code) {
            if (p.first)
                r.dostring(p.second.c_str());
            else
                r.import_explicit(p.second.c_str());
        }
        {
            // save new state in vector of all states
            lock_guard<mutex> lk(m.m_state_mutex);
            m.m_states.push_back(r);
        }
        return r;
    }
}

static void recycle_state(script_state s) {
    if (script_state_manager::is_alive()) {
        script_state_manager & m = get_script_state_manager();
        lock_guard<mutex> lk(m.m_state_mutex);
        m.m_available_states.push_back(s);
    }
}

struct script_state_ref {
    script_state m_state;
    script_state_ref():m_state(get_state()) {}
    ~script_state_ref() { recycle_state(m_state); }
};

// If reset == true,  then reset/release the (script_state) thread local storage
// If reset == false, then return (script_state) thread local
static script_state * get_script_state_ref(bool reset) {
    LEAN_THREAD_PTR(script_state_ref) g_thread_state;
    if (reset) {
        g_thread_state.reset(nullptr);
        return nullptr;
    } else {
        if (!g_thread_state.get())
            g_thread_state.reset(new script_state_ref());
        return &((*g_thread_state).m_state);
    }
}

script_state get_thread_script_state() { return *get_script_state_ref(false); }
void release_thread_script_state() { get_script_state_ref(true); }
}