bollu

Sub-expression "(fun
                   lemma : M.memEffect m (step_sem_tiered ge e s MCFG r) =
                           idM
                             (M.memEffect m (step_sem_tiered ge e s MCFG r))
                 =>
                 reflexive_proper Classes.equiv
                   (M.memEffect m (step_sem_tiered ge e s MCFG r))
                   (idM (M.memEffect m (step_sem_tiered ge e s MCFG r)))
                   lemma
                   (M.memEffect m

bollu

Siddharth
@bollu
15:50
Quick question: If I have an "abstract" law over typeclasses, how do I show Coq that it should apply this law concretely in some case? Example below.

Require Import Omega.
Class SemigroupAction (A: Type) (T: Type)  :=
 {
   combine: A -> A -> A;

bollu

static const int N = 100;
void foo (int A[N * N], int B[N * N], int C[N * N]) {
    for(int i = 0; i < N; i++) {
        for(int j = 0; j < N; j++)
            for(int k = 0; k < N; k++)
                A[i*N + k] += B[i*N + j] * C[j*N + k];
    }
}

bollu

/home/bollu/build/llvm/llvm/tools/polly/test/create_ll.sh scev-2d.c
"/home/bollu/build/llvm/build/bin/opt" -analyze -scalar-evolution scev-2d.ll
Printing analysis 'Scalar Evolution Analysis' for function 'foo':
Classifying expressions for: @foo
  %indvars.iv2 = phi i64 [ %indvars.iv.next3, %for.inc7 ], [ 0, %entry ]
  -->  {0,+,10}<nuw><nsw><%for.cond> U: [0,11) S: [0,11)		Exits: 10		LoopDispositions: { %for.cond: Computable, %for.cond1: Invariant }
  %indvars.iv = phi i64 [ %indvars.iv.next, %for.inc ], [ 0, %for.body ]
  -->  {0,+,1}<nuw><nsw><%for.cond1> U: [0,11) S: [0,11)		Exits: 10		LoopDispositions: { %for.cond1: Computable, %for.cond: Variant }
  %tmp = add nuw nsw i64 %indvars.iv2, %indvars.iv
  -->  {{0,+,10}<nuw><nsw><%for.cond>,+,1}<nw><%for.cond1> U: [0,21) S: [0,21)		Exits: {10,+,10}<nuw><nsw><%for.cond>		LoopDispositions: { %for.cond1: Computable, %for.cond: Variant }

bollu

Error:
Recursive definition of MemD_proper_wrt_eutt is ill-formed.
In environment
X : Type
MemD_proper_wrt_eutt :
forall (x x' : IO.Trace X) (mem : M.memory),
x ≡ x' -> M.memD mem x ≡ M.memD mem x'
x : IO.Trace X
x' : IO.Trace X
mem : M.memory

bollu

Consider the proof term:

M.memD M.empty
    (bindM
       (bindM
          (bindM (Ret (SS.ENV.empty dvalue))
             (fun g : SS.genv =>
              bindM (SS.register_functions program g)
                (fun g2 : SS.genv =>

bollu

Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import AST.
Require Import Cop.
Require Import Cminor.
Require Import Integers.
Require Import SCEV.
Require Import Znat.
Require Import Nat.

bollu

First, use the new exec_looprev to reason about the loop in terms of:

looprev [1..n] = looprev[1..(n-1)]; stmt n

Once we have this, assume:

given:
------
l: exec_loop m IDENTITY_SCHED m1

bollu

# Polly, value profiling

```
===-------------------------------------------------------------------------===
                          ... Statistics Collected ...
===-------------------------------------------------------------------------===

     2 adce                  - Number of branch instructions removed
   900 adce                  - Number of instructions removed
 16302 asm-printer           - Number of machine instrs printed

bollu

CPU (total # of instructions, as counted by -instcount)

• DRAGONEGG_TOTAL_INSTRUCTIONS_CPU = 124996
• POLLY_VALUE_PROFILING_TOTAL_INSTRUCTIONS_CPU = 133760
• POLLY_NO_VALUE_PROFILING_TOTAL_INSTRUCTIONS_CPU = 176316

GPU (total # of instructions, across all kernels)

• gpu total (valprof): 14719
• total (novalprof): 17326

Ratio (GPU / CPU)