Meeting notes 02/07/22 (#3776)

meetings/cranelift/2022/cranelift-02-07.md

@@ -17,5 +17,48 @@
 ## Notes
 
 ### Attendees
+- cfallin
+- avanhatt
+- Monica Pardeshi
+- abrown
+- bnjbvr
+- jlbirch
+- uweigand
+- sparker-arm
+- Fraser Brown
 
 ### Notes
+
+avanhatt presented ISLE SMT rule verification prototype, currently type and term variants for IR-to-IR verification.
+
+- avanhatt: open question, what should the syntax be? LHS, extractor, is more complex.
+- cfallin: Feels like global type inference. Annotations on prelude or standard library, keep them out of lowering rules.
+- avanhatt: Agreed, that it would be good to not have to specify downstream rules.
+- cfallin: Recursion could be a problem.
+- uweigand: Not sure I understand the big picture. How do we define formal semantics of backend ISAs?
+- avanhatt: Current research and tools are available for x86 and Arm.
+- cfallin: We don't even have a good prose descriptions of CLIF operations yet.
+- avanhatt: The Alive project managed without formal semantics.
+- uweigand: Will look to see if there's anything for S390.
+- uweigand: Could the semantics annotations be used to generate the isel code?
+- cfallin: Would depend whether it could produce efficient code, would be good for asserts though.
+- avanhatt: Yes, we could use it for asserts to strengthen fuzzing.
+- FB: Could be used for equivalence checks on rust code too.
+
+# standups
+
+- sparker-arm: Sizeless vector RFC updated, atomics isle porting.
+- uweigand: Branches and traps lowering changes merged. Implemented atomics, which was complicated for narrow types, involved emitting loops.
+        - sparker-arm: Would the SMT verifier be capable of handling loops?
+- uweigand: Still not sure to do about call lowering, as calls can return more than two values.
+        - cfallin: Should we do it?
+        - uweigand: S390 ABI wants extended values and isle could be useful for this.
+        - cfallin: Separate call instruction from arg/return setup..?
+- uweigand: Reorganising ABICaller(Callee?) to simplify the communication between the backend.
+- uweigand: Next moving onto SIMD.
+- abrown: ISLE select lowering for x64, seems like more flag handling infrastructure needs to be added. Now looking at sightglass for instantiation metrics.
+- jlbirch: Worked on a patch for sightglass to automatically trigger benchmarking when a patch is committed. Would like to know why this isn't a good idea for github actions.
+        - cfallin: Need to trust that a PR isn't malicious.
+- bnjbvr: Has been working on ittapi for cross-platform Vtune support.
+        - abrown: Thanks so much for this.
+- cfallin: Will be thinking about isle rule precedence.