From 4dc3764a020d7442ebdc9dc252555aeaf29d92c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Dec 2015 21:16:07 -0800 Subject: [PATCH] feat(util,library,shell): basic locking mechanism We still have to test on Windows. see issue #925 --- src/library/module.cpp | 40 ++++++++++++++++++++++----------------- src/shell/lean.cpp | 8 ++++++++ src/util/CMakeLists.txt | 2 +- src/util/file_lock.cpp | 42 +++++++++++++++++++++++++++++++++++++++++ src/util/file_lock.h | 33 ++++++++++++++++++++++++++++++++ 5 files changed, 107 insertions(+), 18 deletions(-) create mode 100644 src/util/file_lock.cpp create mode 100644 src/util/file_lock.h diff --git a/src/library/module.cpp b/src/library/module.cpp index 12dea2f38b..250949ea59 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "util/buffer.h" #include "util/interrupt.h" #include "util/name_map.h" +#include "util/file_lock.h" #include "kernel/type_checker.h" #include "kernel/quotient/quotient.h" #include "kernel/hits/hits.h" @@ -347,27 +348,32 @@ struct import_modules_fn { throw exception(sstream() << "circular dependency detected at '" << fname << "'"); m_visited.insert(fname); m_imported.insert(fname); - std::ifstream in(fname, std::ifstream::binary); - if (!in.good()) - throw exception(sstream() << "failed to open file '" << fname << "'"); try { - deserializer d1(in); - std::string header; - d1 >> header; - if (header != g_olean_header) - throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file, invalid header"); unsigned major, minor, patch, claimed_hash; - d1 >> major >> minor >> patch >> claimed_hash; - // Enforce version? - - unsigned num_imports = d1.read_unsigned(); + unsigned code_size; buffer imports; - for (unsigned i = 0; i < num_imports; i++) - imports.push_back(read_module_name(d1)); + std::vector code; + { + shared_file_lock fname_lock(fname); + std::ifstream in(fname, std::ifstream::binary); + if (!in.good()) + throw exception(sstream() << "failed to open file '" << fname << "'"); + deserializer d1(in); + std::string header; + d1 >> header; + if (header != g_olean_header) + throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file, invalid header"); + d1 >> major >> minor >> patch >> claimed_hash; + // Enforce version? - unsigned code_size = d1.read_unsigned(); - std::vector code(code_size); - d1.read(code); + unsigned num_imports = d1.read_unsigned(); + for (unsigned i = 0; i < num_imports; i++) + imports.push_back(read_module_name(d1)); + + code_size = d1.read_unsigned(); + code.resize(code_size); + d1.read(code); + } if (m_senv.env().trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL) { unsigned computed_hash = hash(code_size, [&](unsigned i) { return code[i]; }); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index dba6685d6e..a1845c15b7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "util/thread.h" #include "util/thread_script_state.h" #include "util/lean_path.h" +#include "util/file_lock.h" #include "util/sexpr/options.h" #include "util/sexpr/option_declarations.h" #include "kernel/environment.h" @@ -65,6 +66,8 @@ using lean::declaration_index; using lean::keep_theorem_mode; using lean::module_name; using lean::simple_pos_info_provider; +using lean::shared_file_lock; +using lean::exclusive_file_lock; enum class input_kind { Unspecified, Lean, HLean, Lua, Trace }; @@ -463,6 +466,7 @@ int main(int argc, char ** argv) { if (read_cache) { try { cache_ptr = &cache; + shared_file_lock cache_lock(cache_name); std::ifstream in(cache_name, std::ifstream::binary); if (!in.bad() && !in.fail()) cache.load(in); @@ -535,6 +539,7 @@ int main(int argc, char ** argv) { ok = false; } if (save_cache) { + exclusive_file_lock cache_lock(cache_name); std::ofstream out(cache_name, std::ofstream::binary); cache.save(out); } @@ -544,14 +549,17 @@ int main(int argc, char ** argv) { index.save(regular(env, ios)); } if (export_objects && ok) { + exclusive_file_lock output_lock(output); std::ofstream out(output, std::ofstream::binary); export_module(out, env); } if (export_txt) { + exclusive_file_lock expor_lock(*export_txt); std::ofstream out(*export_txt); export_module_as_lowtext(out, env); } if (export_all_txt) { + exclusive_file_lock export_lock(*export_all_txt); std::ofstream out(*export_all_txt); export_all_as_lowtext(out, env); } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 4a5e54faf9..0a6fd56c12 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -5,4 +5,4 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp - null_ostream.cpp) + null_ostream.cpp file_lock.cpp) diff --git a/src/util/file_lock.cpp b/src/util/file_lock.cpp new file mode 100644 index 0000000000..e9326a2d55 --- /dev/null +++ b/src/util/file_lock.cpp @@ -0,0 +1,42 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/exception.h" +#include "util/sstream.h" +#include "util/file_lock.h" +#ifdef _WINDOWS +namespace lean { +file_lock::file_lock(char const *, bool) { + // TODO(Leo): +} +file_lock::~file_lock() { +} +} +#else +#include +#include +namespace lean { +file_lock::file_lock(char const * fname, bool exclusive): + m_fname(fname), m_fd(-1) { + m_fname += ".lock"; + m_fd = open(m_fname.c_str(), O_CREAT, 0xFFFF); + if (m_fd == -1) + throw exception(sstream() << "failed to lock file '" << fname << "'"); + int status = flock(m_fd, exclusive ? LOCK_EX : LOCK_SH); + // TODO(Leo): should we use a loop and keep checking, and fail after k seconds? + if (status == -1) + throw exception(sstream() << "failed to lock file '" << fname << "'"); +} +file_lock::~file_lock() { + if (m_fd != -1) { + std::remove(m_fname.c_str()); + flock(m_fd, LOCK_UN); + close(m_fd); + } +} +} +#endif diff --git a/src/util/file_lock.h b/src/util/file_lock.h new file mode 100644 index 0000000000..bdfab1304f --- /dev/null +++ b/src/util/file_lock.h @@ -0,0 +1,33 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +namespace lean { +/** \brief Helper class for creating an auxiliary lean file and locking it. + We use this object to prevent a lean process from reading a .olean (.ilean/.clean) + file while another one is writing. */ +class file_lock { + std::string m_fname; + int m_fd; +public: + file_lock(char const * fname, bool exclusive); + file_lock(std::string const & fname, bool exclusive):file_lock(fname.c_str(), exclusive) {} + ~file_lock(); +}; + +class exclusive_file_lock : public file_lock { +public: + exclusive_file_lock(char const * fname):file_lock(fname, true) {} + exclusive_file_lock(std::string const & fname):file_lock(fname, true) {} +}; + +class shared_file_lock : public file_lock { +public: + shared_file_lock(char const * fname):file_lock(fname, false) {} + shared_file_lock(std::string const & fname):file_lock(fname, false) {} +}; +}