feat(util,library,shell): basic locking mechanism

We still have to test on Windows.
see issue #925

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<module_name> imports;
-            for (unsigned i = 0; i < num_imports; i++)
-                imports.push_back(read_module_name(d1));
+            std::vector<char> 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<char> 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]; });

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);
         }

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)

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 <string>
+#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 <unistd.h>
+#include <sys/file.h>
+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

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 <string>
+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) {}
+};
+}