OptiGPU

INSTALL.md

@@ -147,7 +147,7 @@ Follow to the next section to test that your OptiTrust installation works.
 
 ## OptiTrust setup
 
-### Install precommit hooks
+### DEPRECATED: Install precommit hooks
 
 This command configures git to automatically run unit tests between commits. It can be ignored if you just want to try OptiTrust without contributing, and you have not downloaded the source files through git.
 
@@ -204,6 +204,7 @@ may want to add into your `~/.bashrc` the line:
 ```
 (or use `sudo ln -s /usr/bin/codium /usr/bin/code`).
 
+NEW : there is now a VSCode extension that can be installed by following the instructions in `tools/vscode-optitrust/README.md`.
 
 ### Direnv setup for automatic Nix shell activation in VSCode (experimental)
 
@@ -222,6 +223,8 @@ Once installed, when you open the OptiTrust repo in VScode, you should first be
 --------------------------------------------------------------------------------
 ## Browser installation
 
+NOTE: not necessary if you use the new VSCode extension.
+
 NOTE: If you're using the Nix shell, don't try to install a browser in the Nix environment, install it on the system as you would normally.
 
 Recommended: installation of Chromium browser, which is very fast for
@@ -281,6 +284,8 @@ Alternatively, use the quick open prompt (`ctrl+p`), then paste `ext install oca
 
 ### Install the OptiTrust shortcuts for VSCode
 
+NOTE: not necessary if you use the new VSCode extension setup.
+
 In VSCode, open the file `~/.config/Code/User/keybindings.json`.
 For VSCodium, this file is located at `~/.config/VSCodium/User/keybindings.json`.
 If you have an empty file, paste the following contents.
@@ -511,6 +516,8 @@ matrix-multiply case study.
 
 ### Viewing keyboard shortcuts
 
+TODO: check if still relevant to the new VSCode extension setup.
+
 It may not be easy at first to recall all the shortcuts. Besides using a sticker
 at the bottom of your screen, you can use the command `./shortcuts.sh` to display
 the shortcuts, and in VSCode use menu File / Preferences / Keyboard Shortcuts,

README.md

@@ -18,10 +18,11 @@ If you are interested in a demo, please get in touch with @charguer.
 # Steps for using OptiTrust
 
 - See `INSTALL.md` for installation procedure, to set up the right version of OCaml/Clang/ClangML and configure VSCode/Codium, in particular.
+- See `tools/vscode-optitrust/README.md` to set up the new VSCode extension (still being refined).
 - See `INSTALL_EXTRA.md` for a list of additional useful tools for program optimization.
 - See `VSCODE_CUSTOMIZE.md` for useful tips for using VScode or VScodium.
 - Read the text below for high level comments on the organization of the repository.
-- Check out `case_studies/matmul/matmul_check.ml` and `matmul_check.cpp` to begin with---to produce a full trace you may need a lot of RAM.
+- Check out `case_studies/dot_product/dot.ml` and `dot.cpp` to begin with---to produce a full trace you may need a lot of RAM.
 
 # Overview of the implementation
 
@@ -59,6 +60,8 @@ In the `tests` and `case_studies` folders, for each unit test and each case stud
 - `_out.cpp` (not committed): contains the optimized code, produced when executing the `.ml` script.
 - `_exp.cpp`: is a git-versioned copy of `_out.cpp`; the tester claims success if the `_out.cpp` matches the `_exp.cpp`; if legitimate changes are applied to the test, the `_exp.cpp` file should be manually updated to match the `_out.cpp` file (e.g., using `cp` or using the dedicated `./tester fixexp` command).
 
+TODO: update paragraphs below
+
 When producing a trace (see shortcuts in `INSTALL.md`), the trace opens in a browser. In the trace display, on a given step, there are options to control the display:
 - mode: `diff` between before-step and after-step, `code before` and `code after` for seeing the code in full before or after the step. If the diff for a step is empty, only the code is displayed.
 - `decode`: to see the internal representation of the AST

case_studies/clift/demo/demo_no_verif.ml

@@ -1,8 +1,10 @@
+(* Deprecated *)
+
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := false;
+  (* Flags.check_validity := false; *)
   Flags.detailed_resources_in_trace := false;
   Flags.pretty_matrix_notation := true
 

case_studies/clift/demo/demo_verif.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := true;
+  (* Flags.check_validity := true; *)
   (* Flags.detailed_resources_in_trace := true; *)
   Flags.save_ast_for_steps := Some Steps_important
 

case_studies/clift/demo/loop_swap.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := true;
+  (* Flags.check_validity := true; *)
   Flags.detailed_resources_in_trace := true;
   Flags.save_ast_for_steps := Some Steps_all
 

case_studies/clift/quantization/access_scale.ml

@@ -1,8 +1,9 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
-let _ = Flags.check_validity := true
-let _ = Flags.recompute_resources_between_steps := true
+(* let _ = Flags.check_validity := true *)
+(* let _ = Flags.recompute_resources_between_steps := true *)
 
 let insert_max_tab_on (tab : typed_var) (size : trm) (i : int) (t : trm) : trm =
   let v, typ = tab in

case_studies/clift/quantization/matvec_to_quantize.ml

@@ -1,10 +1,11 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
   Flags.pretty_matrix_notation := true;
   Flags.print_optitrust_syntax := true;
-  Flags.check_validity := false
+  (* Flags.check_validity := false *)
 
 let reconstruct_seq (lbefore : trm mlist) (t : trm) (lafter : trm mlist) : trm =
   let new_lbefore = Mlist.push_back t lbefore in

case_studies/clift/verif/kernels.ml

@@ -1,7 +1,8 @@
+(* Deprecated *)
 open Optitrust
 open Prelude
 
 let _ =
-  Flags.check_validity := true;Flags.detailed_resources_in_trace := true;
+ (*  Flags.check_validity := true; *)Flags.detailed_resources_in_trace := true;
 Flags.save_ast_for_steps := Some Steps_all
 let _  = Run.script_cpp ( fun x -> !!!());

case_studies/dot_product/README.md

@@ -0,0 +1,175 @@
+============================HIGH LEVEL VIEW OF THE SCRIPT ==============
+
+s = 0
+__ghost(0 = reduce(0,0,f) à réécrire dans s ~> 0 pour avoir s ~> reduce(0,0,..))
+for i
+  __invariant "s ~> reduce(0,i,...)"
+  s += a[i] * b[i]
+  __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de s)
+
+--- unfold infix ops
+
+s = 0
+for i
+  __invariant "s ~> reduce(0,i,...)"
+  s = s + a[i] * b[i]
+
+--- tile
+const int NB_BLOCK = a.length/B // to insert! with check divisibility?
+s = 0
+for b = 0 to NB_BLOCK
+  __invariant "s ~> reduce(0,b*B,...)"
+  for i = b*B to (b+1)*B
+    __invariant "s ~> reduce(0,i,...)"
+    s = s + a[i] * b[i]
+    __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de s)
+
+--- local name
+
+s = 0
+for b
+  __invariant "s ~> reduce(0,b*B,...)"
+  t = s
+  // ghost(hide_cell, consume s~>v, produces "hidden(s,t)")
+  for i = b*B to (b+1)*B
+    __invariant "t ~> reduce(0,i,...)"
+    t = t + a[i] * b[i]
+    __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de t)
+  s = t
+  // ghost(hide_rev_cell, consume hidden(s,t), consume(t->w), produces "s~>w")
+
+--- insert def 'p' for the contents of 's'
+
+s = 0
+for b
+  __invariant "s ~> reduce(0,b*B,...)"
+  const int p = s;  // sum of the prefix upto the block b
+  // in ctx, we have an alias: "p := reduce(0,b*B,...)"
+  t = s
+  for i = b*B to (b+1)*B
+    __invariant "t ~> reduce(0,i,...)"
+    t = t + a[i] * b[i]
+    __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de t)
+  s = t
+
+--- shift_var t by p
+
+s = 0
+for b
+  __invariant "s ~> reduce(0,b*B,...)"
+  const int p = s
+  // in ctx, we have an alias: "p := reduce(0,b*B,...)"
+  t = s - p // -p on write into t
+  for i = b*B to (b+1)*B
+    __invariant "t ~> reduce(0,i,...) - p" // -p on models of t
+    t = ((t + p) + a[i] * b[i]) - p   // +p on reads on t, -p on write into t
+    // ICI problème: on avait
+    // __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de t)
+    // et maintenant il faut
+    // __ghost(reduce(0,i,f) - p + p + f(i) - p = reduce(0,i+1,f) - p à réécrire dans le contenu de t)
+    // ça je sais pas trop comment on va gérer... peut être sans typer les étapes intermédiaires ?
+    // parce que après on retrouve un moment où la ghost d'origine fonctionne telle quelle
+  s = t + p  // +p on reads on t
+
+
+--- unfold def of 'p' in the code (not in formulae), using the fact that s is not modified in the scope
+
+s = 0
+for b
+  __invariant "s ~> reduce(0,b*B,...)"
+  const int p = s
+  // in ctx, we have an alias: "p := reduce(0,b*B,...)"
+  t = s - s
+  // in ctx, we have t ~> reduce(0,b*B,...) - reduce(0,b*B,...)
+  for i = b*B to (b+1)*B
+    __invariant "t ~> reduce(0,i,...) - p"
+    t = ((t + s) + a[i] * b[i]) - s
+    // ... ici la ghost qui va bien
+  s = t + s
+
+-- remove s from the block-processing by arith_simpl
+
+s = 0
+for b
+  __invariant "s ~> reduce(0,b*B,...)"
+  const int p = s
+  // in ctx, we have an alias: "p := reduce(0,b*B,...)"
+  t = 0
+  // HERE: need to insert a ghost rewriting "0" into "reduce(0,b*B,...) - reduce(0,b*B,...)" in contents of t
+  for i = b*B to (b+1)*B
+    __invariant "t ~> reduce(0,i,...) - p"
+    t = t + a[i] * b[i]
+    // la ghost d'accumulation fonctionne de nouveau !
+    __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de t)
+  s = t + s
+
+--- optional step: turn "p" into ghost def;
+--    alternative: inline "p", replacing it with "reduce(0,b*B,...)" in the formulae
+--    if we do nothing, it's fine too, but we'll need to duplicate "const int p = s"
+      when we do the fusion step later.
+
+s = 0
+for b
+  __invariant "s ~> reduce(0,b*B,...)"
+  // BEFORE:
+  //   const int p = s  // where p is not used in the code, only in formulae
+  //   in ctx, we have an alias: "p := reduce(0,b*B,...)"
+  // AFTER:
+  //   __DEF(p, "reduce(0,b*B,...)");
+  ...
+
+  ==> in fine, I think inlining 'p' into 'reduce(0,b*B,...)' in formulae would be easiest.
+
+
+--- hoist de t
+
+s = 0
+alloc t as an array of NB_BLOCK
+for b
+  __xmodifies "t ~> UninitCell" // pas de spécification du modèle d'entrée ou de sortie
+  __invariant "s ~> reduce(0,b*B,...)"
+  t[b] = 0
+  // ghost rewriting "0" into "reduce(0,b*B,...) - reduce(0,b*B,...)" in contents of t
+  for i = b*B to (b+1)*B
+    __invariant "t[b] ~> reduce(0,i,...) - reduce(0,b*B,...)" // MODIFIED CONTRACT: t becomes t[b]
+    t[b] = t[b] + a[i] * b[i]
+    __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de t)
+  // NOTE: at this point, the ctx stores t[b] ~> reduce(0,i,...) - reduce(0,b*B,...)
+  //   the value of t[b] determines the contract for the fission that comes next
+  s = t[b] + s
+
+
+--- fission + parallelization
+
+s = 0
+alloc t as an array of NB_BLOCK
+parallel for b
+  __xmodifies "t[b] ~> t[b] ~> reduce(0,i,...) - reduce(0,b*B,...)" // NEW CONTRACT!
+  __DEF(p, "reduce(0,b*B,...)");
+  t[b] = 0
+  // ghost rewriting "0" into "reduce(0,b*B,...) - reduce(0,b*B,...)" in contents of t
+  for i = b*B to (b+1)*B
+    __invariant "t ~> reduce(0,i,...) - reduce(0,b*B,...)"
+    t[b] = t[b] + a[i] * b[i]
+    __ghost(reduce(0,i,f) + f(i) = reduce(0,i+1,f) à réécrire dans le contenu de t)
+for b
+  // MOVED: contract on 's' is just moved here
+  __invariant "s ~> reduce(0,b*B,...)"
+  s = t[b] + s
+
+
+--- cleanup, with infix ops
+
+s = 0
+alloc t as an array of NB_BLOCK
+parallel for b
+  t[b] = 0
+  for i = b*B to (b+1)*B
+    t[b] += a[i] * b[i]
+for b
+  s += t[b]
+
+
+=====================
+# remark: it seems that we never need to exploit
+   "reduce(0,i,f) - reduce(0,j,f) = reduce(j,i,f)"

case_studies/dot_product/dot.cpp

@@ -3,7 +3,6 @@
 __DECL(reduce_sum, "int * (int -> float) -> float");
 __AXIOM(reduce_sum_empty, "forall (f: int -> float) -> 0.f =. reduce_sum(0, f)");
 __AXIOM(reduce_sum_add_right, "forall (n: int) (f: int -> float) (_: n >= 0) -> reduce_sum(n, f) +. f(n) =. reduce_sum(n + 1, f)");
-__DEF(matmul, "fun (A B: int * int -> float) (p: int) -> fun (i j: int) -> reduce_sum(p, fun k -> A(i, k) *. B(k, j))");
 
 /* Multiplies the vect A (dim n) by the vector B (dim n),
  * and returns the result of the scalar product.