Added SMT query hashes to hints to skip unchanged queries. #1257

wintersteiger · 2017-09-21T18:17:54Z

@nikswamy: the basic functionality is in place. Whenever the hashes match, it reports Query-stats ... succeeded (with hint) ... statistics={fstar_cache_hit=1}. It will also read old hints and then update them with hashes when --record_hints is on. It will use hashes whenever --use_hints is on, but I suppose it would be a good idea to add a command-line parameter to "opt in".

nikswamy · 2017-09-22T17:31:19Z

Hi Christoph,

Many thanks for this feature.

In its current form, the PR is very hard to review since it contains many auto-generated files (.ml, .hints etc.)

Do you think you could submit another version of the PR with just the changes that actually need to be reviewed?

As for timing: I would wait for the ongoing Everest merge to stabilize and then try to update our projects and all hints to use this feature.

A question: will it possible to re-use old hint files with this feature turned off (i.e., just --use_hints with old hint files). Or, are we forced to upgrade all hint files as soon as this feature lands?

Thanks,
Nik

wintersteiger · 2017-09-22T20:08:52Z

Agreed, it's a bit of a mess at the moment. I checked in new snapshot files because the extraction that worked perfectly fine on my machine didn't go through the CI for reasons that weren't obvious from the log files. I may have been using a different version of OCaml or some such thing.

Feature-wise, yes, old hint files will be read in exactly the same way as before when --use_hints is on. They will only be upgraded with the extra hash field when --record_hints is on. I also added --use_hint_hashes so the by default the behavior is exactly the same as before. Something's still wrong with that flag though, so don't merge just yet.

nikswamy · 2017-09-26T04:16:33Z

We've completed the Everest merge of last week. So, I'd be happy to have this feature completed and merged in as soon as you're done.

wintersteiger · 2017-09-27T10:37:20Z

Working on this, should be done by the end of today!

wintersteiger · 2017-09-27T19:42:52Z

Features are there, but the OCaml extraction still won't work on the CI machine and I'm not getting any useful error messages. Apparently, the snapshot code extracts different code from the same sources when run on the CI machine, but so far I wasn't able to determine why.

cpitclaudel · 2017-09-29T07:39:39Z

Nik, there's a dropdown in the Github UI that allows you to pick which commits to display :) Just exclude the snapshot commit.

cpitclaudel · 2017-09-29T07:42:20Z

I'm excited about this feature :) IIUC, it's essentially an implementation of #1140, right?

How well will this work with the interactive mode? Are the caches constructed as we go, so that reprocessing the same query will now be much faster? That would be particularly nice.

cpitclaudel · 2017-09-29T07:43:17Z

src/basic/FStar.Options.fs

@@ -766,6 +768,11 @@ let rec specs () : list<Getopt.opt> =
        "Use a previously recorded hints database for proof replay");

       ( noshort,
+        "use_hint_hashes",
+        ZeroArgs (fun () -> mk_bool true),


I've just merged a change to master that will conflict with this line. The fix is to use Const (mk_bool true) instead of ZeroArgs (mk_bool true)

Did you rename/remove ZeroArgs? I'll have to re-merge with master anyways, so will be fixed imminently.

I added a layer on top of ZeroArgs / OneArg. Const gets interpreted into ZeroArgs.

cpitclaudel · 2017-09-29T07:44:25Z

src/basic/boot/FStar.Util.fs

-                if (Array.length ha) <> 6 then failwith "malformed hint" else
-                Some {
+                if (Array.length ha) <> 6 && (Array.length ha) <> 7
+                then failwith "malformed hint"


Can we raise an error instead?

That's what the old implementation did... what kind of error would you prefer?

I'm not sure. Either it's OK to continue without the hint, in which case we could simply issue a warning and go on; or we want to fail, but in that case it'd be nice to include the file name of the hint file.

I noticed this while reading through, but indeed I wasn't criticizing a new addition :)

cpitclaudel · 2017-09-29T07:45:36Z

src/basic/ml/FStar_Util.ml

+                                            | `List strings ->
+                                               Some (List.map (function
+                                                         | `String s -> s
+                                                         | _ -> raise Exit


One problem with using Exceptions for control flow like this is that it yields very slow Javascript when we extract. But I think this code doesn't get run a lot, right?

Yep, that runs once while reading the hints file.

cpitclaudel · 2017-09-29T07:46:37Z

src/smtencoding/FStar.SMTEncoding.Z3.fs

+      z3status
+    * int
+    * z3statistics
+    * option<string> // query hash


Past two/three fields, I tend to like records better (though I agree that adding the extra type is already a plus)

I have no opinion about that, happy to change it to records if that's preferred.

cpitclaudel · 2017-09-29T07:47:26Z

src/smtencoding/FStar.SMTEncoding.Z3.fs

@@ -498,29 +504,67 @@ let refresh () =
        bg_scope := List.flatten (List.rev !fresh_scope)

 let mk_input theory =
+    let query_hash =
+        if Options.record_hints() || (Options.use_hints() && Options.use_hint_hashes()) then (
+            let ft = (fun x -> match x with


This could just be function instead of fun x -> match x with

cpitclaudel · 2017-09-29T07:49:34Z

We have this bit in the interactive mode:

  if FStar.Options.record_hints() || FStar.Options.use_hints() then
    FStar.SMTEncoding.Solver.with_hints_db (List.hd (Options.file_list ()))
      (fun () -> go init_st)
  else
    go init_st

Does it need to be updated?

s-zanella · 2017-09-29T10:09:44Z

I second Clement's excitement about this feature. If this could be made to work well in interactive, it would be a big productivity boost. But F* generates fresh identifiers on the fly, so as for now a query issued a second time will differ syntactically (mostly alpha-renaming, I believe) from the first time it was ran.

cpitclaudel · 2017-09-29T12:43:32Z

But F* generates fresh identifiers on the fly, so as for now a query issued a second time will differ syntactically (mostly alpha-renaming, I believe) from the first time it was ran.

Good point. I don't expect this would be so hard to fix, though — probably just an issue of rolling back the gensyms when we step back in the interactive mode

wintersteiger · 2017-09-29T13:26:02Z

@cpitclaudel: I think that part should be fine, we still need to load the hints, regardless of whether we use or ignore the hashes.

@s-zanella: Absolutely! There are some issues to think about, e.g. variable renaming, ordering, incrementality, etc, but I'm sure we can come up with something that's useful in interactive mode as well.

wintersteiger · 2017-09-29T13:48:51Z

Just pushed a few improvements. This version takes less memory (smt2-string only generated once), but it's still not quite as fast as I'd like it to be. Ideas for optimizations are most welcome!

cpitclaudel · 2017-09-29T14:14:16Z

Can you rebase and move the snapshot to the end? Or is there a way on github to exclude a snapshot that's in the middle of the history?

wintersteiger · 2017-09-29T14:18:54Z

I don't think so, that would break the history. I can force-push after I hack the history locally, but I wouldn't want to do that after comments have been added (I think they would just disappear). The changes in fd15e83 are very small and local though.

nikswamy · 2017-09-29T16:02:04Z

Regarding this question from @cpitclaudel

We have this bit in the interactive mode:

  if FStar.Options.record_hints() || FStar.Options.use_hints() then
    FStar.SMTEncoding.Solver.with_hints_db (List.hd (Options.file_list ()))
      (fun () -> go init_st)
  else
    go init_st

Does it need to be updated?

I don't think so. The new feature is only enabled under FStar.Options.use_hints() && FStar.Options.use_hint_hashes(). So, this code should be ok as is.

wintersteiger · 2017-09-29T16:09:27Z

@nikswamy thanks for adding comments, I totally neglected that part of the job!

…list reversal actually makes a huge difference here, with lists of 100k elements; goes from 450ms per query to about 15ms and changes to overall replay time for long files like FStar.Pointer.Base from 4.5min to 1min

…fix makefiles in tutorial to be parallel and to pass options in from caller

…8-9 minutes to run on its own

… Canon.Test)

wintersteiger self-assigned this Sep 21, 2017

wintersteiger requested a review from nikswamy September 21, 2017 18:17

wintersteiger force-pushed the cwinter_query_hashes branch 2 times, most recently from 0f0bdfa to 405e21e Compare September 27, 2017 18:55

Added query hashes in hint files; use them with --use_hint_hashes

780f61d

wintersteiger force-pushed the cwinter_query_hashes branch from 405e21e to 780f61d Compare September 27, 2017 18:59

Updated snapshot

e1fde8e

cpitclaudel reviewed Sep 29, 2017

View reviewed changes

Merged master into cwinter_query_hashes

82ed037

Christoph M. Wintersteiger added 2 commits September 29, 2017 14:29

Improvements to hint hashes.

fd15e83

New snapshot

8692456

nikswamy added 2 commits September 29, 2017 09:03

some refactorings, comments and formatting changes

590512d

snap

57757e7

add a message tag to measure_execution_time

ac9e7db

nikswamy added 11 commits September 29, 2017 10:57

new hints with query hashes

b56e60e

turn on --use_hint_hashes by default in our makefiles

463f96c

new hints with query hashes

d41aadb

allow queries to be replayed using hashes even after a hint failure; …

94ffa8b

…fix makefiles in tutorial to be parallel and to pass options in from caller

temporarily disable Canon.Test from the test suite; it takes 3GB and …

fe415f0

…8-9 minutes to run on its own

snap

a655f71

reordering targets in ulib to make the expensive ones go first

b877626

new hints

999e0cf

hints

3f7024a

restore native tactics test (although it still takes very long to run…

50ff9be

… Canon.Test)

nikswamy merged commit 50ff9be into master Sep 29, 2017

catalin-hritcu deleted the cwinter_query_hashes branch April 7, 2018 14:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added SMT query hashes to hints to skip unchanged queries. #1257

Added SMT query hashes to hints to skip unchanged queries. #1257

wintersteiger commented Sep 21, 2017

nikswamy commented Sep 22, 2017

wintersteiger commented Sep 22, 2017

nikswamy commented Sep 26, 2017

wintersteiger commented Sep 27, 2017

wintersteiger commented Sep 27, 2017

cpitclaudel commented Sep 29, 2017

cpitclaudel commented Sep 29, 2017

cpitclaudel Sep 29, 2017

wintersteiger Sep 29, 2017

cpitclaudel Sep 29, 2017

cpitclaudel Sep 29, 2017

wintersteiger Sep 29, 2017

cpitclaudel Sep 29, 2017

cpitclaudel Sep 29, 2017

wintersteiger Sep 29, 2017

cpitclaudel Sep 29, 2017

wintersteiger Sep 29, 2017

cpitclaudel Sep 29, 2017

cpitclaudel commented Sep 29, 2017

s-zanella commented Sep 29, 2017

cpitclaudel commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

cpitclaudel commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

nikswamy commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

Added SMT query hashes to hints to skip unchanged queries. #1257

Added SMT query hashes to hints to skip unchanged queries. #1257

Conversation

wintersteiger commented Sep 21, 2017

nikswamy commented Sep 22, 2017

wintersteiger commented Sep 22, 2017

nikswamy commented Sep 26, 2017

wintersteiger commented Sep 27, 2017

wintersteiger commented Sep 27, 2017

cpitclaudel commented Sep 29, 2017

cpitclaudel commented Sep 29, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel commented Sep 29, 2017

s-zanella commented Sep 29, 2017

cpitclaudel commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

cpitclaudel commented Sep 29, 2017

wintersteiger commented Sep 29, 2017

nikswamy commented Sep 29, 2017

wintersteiger commented Sep 29, 2017