From 049f2d07fe2e93e1f3ce9e9997c5e1cda3798648 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Feb 2024 12:10:38 -0600 Subject: [PATCH] Use FILE * instead of filenames when passing file paths to serialization and printing commands (#968) Previously we were storing a filename in a global variable and then passing it to a bunch of functions. Each of these functions then had to call fopen and fclose, which was quite expensive. This PR changes the behavior so instead we once open a file with fopen at the start of rewriting, then call a bunch of functions which take a `FILE *` as an argument, then call fclose once at the end. This gets much better buffering behavior and reduces the number of syscalls considerably. When measuring the performance of this code against a "sum to 10k" imp program with proof hint generation enabled, we saw a time reduction from 3.5m to 2m. --- bindings/python/runtime.cpp | 4 +++- include/runtime/header.h | 20 +++++++----------- runtime/finish_rewriting.ll | 5 +++-- runtime/main/main.ll | 7 ++++-- runtime/main/search.cpp | 12 ++++++----- runtime/util/ConfigurationPrinter.cpp | 27 ++++-------------------- runtime/util/ConfigurationSerializer.cpp | 23 +++++--------------- runtime/util/util.cpp | 5 +---- 8 files changed, 36 insertions(+), 67 deletions(-) diff --git a/bindings/python/runtime.cpp b/bindings/python/runtime.cpp index 22231e485..68e75c3b9 100644 --- a/bindings/python/runtime.cpp +++ b/bindings/python/runtime.cpp @@ -96,7 +96,9 @@ void bind_runtime(py::module_ &m) { .def( "_serialize_raw", [](block *term, std::string const &filename, std::string const &sort) { - serializeRawTermToFile(filename.c_str(), term, sort.c_str()); + FILE *file = fopen(filename.c_str(), "a"); + serializeRawTermToFile(file, term, sort.c_str()); + fclose(file); }); } diff --git a/include/runtime/header.h b/include/runtime/header.h index b6d9271d6..dec19e6d9 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -293,10 +293,9 @@ extern "C" { block *parseConfiguration(char const *filename); block *deserializeConfiguration(char *, size_t); -void printConfiguration(char const *filename, block *subject); -void printStatistics(char const *filename, uint64_t steps); +void printConfiguration(FILE *file, block *subject); +void printStatistics(FILE *file, uint64_t steps); string *printConfigurationToString(block *subject); -void printConfigurationToFile(FILE *, block *subject); void printSortedConfigurationToFile( FILE *file, block *subject, char const *sort); void printConfigurationInternal( @@ -325,18 +324,15 @@ string *debug_print_term(block *subject, char const *sort); mpz_ptr move_int(mpz_t); void serializeConfigurations( - char const *filename, std::unordered_set results); + FILE *file, std::unordered_set results); void serializeConfiguration( block *subject, char const *sort, char **data_out, size_t *size_out, bool emit_size); -void serializeConfigurationToFile( - char const *filename, block *subject, bool emit_size); -void writeUInt64ToFile(char const *filename, uint64_t i); -void serializeTermToFile( - char const *filename, block *subject, char const *sort); -void serializeRawTermToFile( - char const *filename, void *subject, char const *sort); -void printVariableToFile(char const *filename, char const *varname); +void serializeConfigurationToFile(FILE *file, block *subject, bool emit_size); +void writeUInt64ToFile(FILE *file, uint64_t i); +void serializeTermToFile(FILE *file, block *subject, char const *sort); +void serializeRawTermToFile(FILE *file, void *subject, char const *sort); +void printVariableToFile(FILE *file, char const *varname); // The following functions have to be generated at kompile time // and linked with the interpreter. diff --git a/runtime/finish_rewriting.ll b/runtime/finish_rewriting.ll index 3d7de729a..a6f312aa2 100644 --- a/runtime/finish_rewriting.ll +++ b/runtime/finish_rewriting.ll @@ -7,10 +7,10 @@ target triple = "@BACKEND_TARGET_TRIPLE@" declare void @printStatistics(i8*, i64) declare void @printConfiguration(i8*, %block*) -declare void @printConfigurationToFile(i8*, %block*) declare void @serializeConfigurationToFile(i8*, %block*) declare void @exit(i32) #0 declare void @abort() #0 +declare void @fclose(i8*) declare i64 @__gmpz_get_ui(%mpz*) declare i8* @getStderr() @@ -37,7 +37,7 @@ define void @finish_rewriting(%block* %subject, i1 %error) #0 { br i1 %isnull, label %abort, label %print abort: %stderr = call i8* @getStderr() - call void @printConfigurationToFile(i8* %stderr, %block* %subject) + call void @printConfiguration(i8* %stderr, %block* %subject) call void @abort() unreachable print: @@ -68,6 +68,7 @@ exitCode: br label %exit exit: %exit_ui = phi i32 [ %exit_trunc, %exitCode ], [ 113, %tail ] + call void @fclose(i8* %output) call void @exit(i32 %exit_ui) unreachable } diff --git a/runtime/main/main.ll b/runtime/main/main.ll index fa2047e10..3209c28d3 100644 --- a/runtime/main/main.ll +++ b/runtime/main/main.ll @@ -6,6 +6,7 @@ target triple = "@BACKEND_TARGET_TRIPLE@" declare %block* @parseConfiguration(i8*) declare i64 @atol(i8*) +declare i8* @fopen(i8*, i8*) declare %block* @take_steps(i64, %block*) declare void @finish_rewriting(%block*, i1) #0 @@ -19,6 +20,7 @@ declare void @printProofHintHeader(i8*) @proof_out.flag = private constant [15 x i8] c"--proof-output\00" @output_file = external global i8* +@a_str = private constant [2 x i8] c"a\00" @statistics = external global i1 @binary_output = external global i1 @proof_output = external global i1 @@ -87,7 +89,8 @@ entry: %depth = call i64 @atol(i8* %depth_str) %output_ptr = getelementptr inbounds i8*, i8** %argv, i64 3 %output_str = load i8*, i8** %output_ptr - store i8* %output_str, i8** @output_file + %output_file = call i8* @fopen(i8* %output_str, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @a_str, i64 0, i64 0)) + store i8* %output_file, i8** @output_file call void @parse_flags(i32 %argc, i8** %argv) @@ -96,7 +99,7 @@ entry: %proof_output = load i1, i1* @proof_output br i1 %proof_output, label %if, label %else if: - call void @printProofHintHeader(i8* %output_str) + call void @printProofHintHeader(i8* %output_file) br label %else else: %ret = call %block* @parseConfiguration(i8* %filename) diff --git a/runtime/main/search.cpp b/runtime/main/search.cpp index 4a87d6580..69071746d 100644 --- a/runtime/main/search.cpp +++ b/runtime/main/search.cpp @@ -11,10 +11,10 @@ uint64_t get_steps(void); std::unordered_set take_search_steps( bool executeToBranch, int64_t depth, int64_t bound, block *subject); void printConfigurations( - char const *filename, std::unordered_set results); + FILE *file, std::unordered_set results); void serializeConfigurations( - char const *filename, std::unordered_set results); + FILE *file, std::unordered_set results); static bool hasStatistics = false; static bool binaryOutput = false; @@ -51,13 +51,15 @@ int main(int argc, char **argv) { block *input = parseConfiguration(filename); std::unordered_set results = take_search_steps(executeToBranch, depth, bound, input); + FILE *file = fopen(output, "w"); if (hasStatistics) { - printStatistics(output, get_steps()); + printStatistics(file, get_steps()); } if (binaryOutput) { - serializeConfigurations(output, results); + serializeConfigurations(file, results); } else { - printConfigurations(output, results); + printConfigurations(file, results); } + fclose(file); return 0; } diff --git a/runtime/util/ConfigurationPrinter.cpp b/runtime/util/ConfigurationPrinter.cpp index 7fabc6933..8408ad8cf 100644 --- a/runtime/util/ConfigurationPrinter.cpp +++ b/runtime/util/ConfigurationPrinter.cpp @@ -183,20 +183,15 @@ void printConfigurationInternal( sfprintf(file, ")"); } -void printStatistics(char const *filename, uint64_t steps) { - FILE *file = fopen(filename, "w"); +void printStatistics(FILE *file, uint64_t steps) { fmt::print(file, "{}\n", steps - 1); // off by one adjustment - fclose(file); } -void printConfiguration(char const *filename, block *subject) { - FILE *file = fopen(filename, "a"); +void printConfiguration(FILE *file, block *subject) { auto state = print_state(); writer w = {file, nullptr}; printConfigurationInternal(&w, subject, nullptr, false, &state); - - fclose(file); } // If the parameter `results` is passed by reference, the ordering induced by @@ -205,8 +200,7 @@ void printConfiguration(char const *filename, block *subject) { // code is not on a hot path. // NOLINTBEGIN(performance-unnecessary-value-param) void printConfigurations( - char const *filename, std::unordered_set results) { - FILE *file = fopen(filename, "a"); + FILE *file, std::unordered_set results) { auto state = print_state(); writer w = {file, nullptr}; @@ -224,8 +218,6 @@ void printConfigurations( } sfprintf(&w, ")"); } - - fclose(file); } // NOLINTEND(performance-unnecessary-value-param) @@ -253,12 +245,6 @@ string *printConfigurationToString(block *subject) { return hook_BUFFER_toString(buf); } -void printConfigurationToFile(FILE *file, block *subject) { - auto state = print_state(); - writer w = {file, nullptr}; - printConfigurationInternal(&w, subject, nullptr, false, &state); -} - void printSortedConfigurationToFile( FILE *file, block *subject, char const *sort) { auto state = print_state(); @@ -334,13 +320,8 @@ void printValueOfType( } } -void printVariableToFile(char const *filename, char const *varname) { - FILE *file = fopen(filename, "a"); - +void printVariableToFile(FILE *file, char const *varname) { fmt::print(file, "{}", varname); char n = 0; fwrite(&n, 1, 1, file); - fflush(file); - - fclose(file); } diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 35cca58bf..5c44a8483 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -367,8 +367,7 @@ void serializeConfigurationInternal( } void serializeConfigurations( - char const *filename, std::unordered_set results) { - FILE *file = fopen(filename, "w"); + FILE *file, std::unordered_set results) { auto state = serialization_state(); auto w = writer{file, nullptr}; @@ -394,20 +393,16 @@ void serializeConfigurations( fwrite(buf, 1, buf_size, file); free(buf); - fclose(file); } -void serializeConfigurationToFile( - char const *filename, block *subject, bool emit_size) { +void serializeConfigurationToFile(FILE *file, block *subject, bool emit_size) { char *data = nullptr; size_t size = 0; serializeConfiguration(subject, nullptr, &data, &size, emit_size); - FILE *file = fopen(filename, "a"); fwrite(data, 1, size, file); free(data); - fclose(file); } void serializeConfiguration( @@ -430,38 +425,30 @@ void serializeConfiguration( *size_out = size; } -void writeUInt64ToFile(char const *filename, uint64_t i) { - FILE *file = fopen(filename, "a"); +void writeUInt64ToFile(FILE *file, uint64_t i) { fwrite(&i, 8, 1, file); - fclose(file); } -void serializeTermToFile( - char const *filename, block *subject, char const *sort) { +void serializeTermToFile(FILE *file, block *subject, char const *sort) { char *data = nullptr; size_t size = 0; serializeConfiguration(subject, sort, &data, &size, true); - FILE *file = fopen(filename, "a"); fwrite(data, 1, size, file); free(data); - fclose(file); } -void serializeRawTermToFile( - char const *filename, void *subject, char const *sort) { +void serializeRawTermToFile(FILE *file, void *subject, char const *sort) { block *term = constructRawTerm(subject, sort, true); char *data = nullptr; size_t size = 0; serializeConfiguration(term, "SortKItem{}", &data, &size, true); - FILE *file = fopen(filename, "a"); fwrite(data, 1, size, file); free(data); - fclose(file); } std::shared_ptr diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp index 351c924c4..df9442c4c 100644 --- a/runtime/util/util.cpp +++ b/runtime/util/util.cpp @@ -38,12 +38,9 @@ block *constructRawTerm(void *subject, char const *sort, bool raw_value) { return static_cast(constructCompositePattern(tag, args)); } -void printProofHintHeader(char *output_file) { +void printProofHintHeader(FILE *file) { uint32_t version = 4; - FILE *file = fopen(output_file, "a"); fmt::print(file, "HINT"); fwrite(&version, sizeof(version), 1, file); - fflush(file); - fclose(file); } }