From cb4bf4443f0c0d3065090a64f67a69e8fa677df1 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 26 Oct 2018 07:29:18 -0700 Subject: [PATCH] [sqlite] increase timeout to avoid BUSY errors Summary: This should stop the bleeding until we get a better solution like shared memory + single writer process. Reviewed By: mbouaziz Differential Revision: D10868360 fbshipit-source-id: a4d0b064e --- infer/man/man1/infer-analyze.txt | 2 +- infer/man/man1/infer-capture.txt | 2 +- infer/man/man1/infer-full.txt | 2 +- infer/man/man1/infer-run.txt | 2 +- infer/man/man1/infer.txt | 2 +- infer/src/base/Config.ml | 7 ++++++- 6 files changed, 11 insertions(+), 6 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 026c8b083..403dd1f4f 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -299,7 +299,7 @@ OPTIONS --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. - (default: 10000) + (default: five seconds times number of cores) --starvation Activates: starvation analysis (Conversely: --no-starvation) diff --git a/infer/man/man1/infer-capture.txt b/infer/man/man1/infer-capture.txt index 1dd441f1c..887c27dbd 100644 --- a/infer/man/man1/infer-capture.txt +++ b/infer/man/man1/infer-capture.txt @@ -97,7 +97,7 @@ OPTIONS --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. - (default: 10000) + (default: five seconds times number of cores) -- Stop argument processing, use remaining arguments as a build command diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 828221642..7fcd057f1 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -834,7 +834,7 @@ OPTIONS --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. - (default: 10000) See also infer-analyze(1), infer-capture(1), and infer-run(1). + (default: five seconds times number of cores) See also infer-analyze(1), infer-capture(1), and infer-run(1). --stacktrace file File path containing a json-encoded Java crash stacktrace. Used to diff --git a/infer/man/man1/infer-run.txt b/infer/man/man1/infer-run.txt index 679915386..a5abab832 100644 --- a/infer/man/man1/infer-run.txt +++ b/infer/man/man1/infer-run.txt @@ -139,7 +139,7 @@ OPTIONS --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. - (default: 10000) + (default: five seconds times number of cores) --version Print version information and exit diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 19235a0ce..da81e55fb 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -834,7 +834,7 @@ OPTIONS --sqlite-lock-timeout int Timeout for SQLite results database operations, in milliseconds. - (default: 10000) See also infer-analyze(1), infer-capture(1), and infer-run(1). + (default: five seconds times number of cores) See also infer-analyze(1), infer-capture(1), and infer-run(1). --stacktrace file File path containing a json-encoded Java crash stacktrace. Used to diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 4d117210f..27edb8234 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2018,7 +2018,12 @@ and specs_library = and sqlite_lock_timeout = - CLOpt.mk_int ~long:"sqlite-lock-timeout" ~default:10_000 + (* some lame estimate: when the frontend writes CFGs to disk, it may take a few seconds to write + one CFG and all the cores may be trying to write to the database at the same time. This means + one process might wait (a few seconds) * (number of cores) to write its CFG. *) + let five_seconds_per_core = ncpu * 5_000 in + CLOpt.mk_int ~long:"sqlite-lock-timeout" ~default:five_seconds_per_core + ~default_to_string:(fun _ -> "five seconds times number of cores") ~in_help: InferCommand.[(Analyze, manual_generic); (Capture, manual_generic); (Run, manual_generic)] "Timeout for SQLite results database operations, in milliseconds."