Skip to content

Instantly share code, notes, and snippets.

View bollu's full-sized avatar

Siddharth bollu

View GitHub Profile
@bollu
bollu / coinduction-with-setoid.v
Created June 22, 2018 16:19
Coinduction fails guardedness condition due to setoid
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
bollu / coq_typeclas_instance
Last active June 15, 2018 13:58
How do I resolve the concrete typeclass case wrt to SemigroupAction?
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;
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
bollu / scev output
Last active June 4, 2018 19:01
Analyzing SCEV of a 2d loop
/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
bollu / corecursive-guard.coq
Created May 31, 2018 21:21
How does one debug corecursive guard condition failing?
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

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
bollu / coq-proof-eliminate-skip.v
Created May 16, 2018 11:03
A proof that shows the requirement to unshelve existentials
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.

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
# 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
bollu / static-instr-numbers.md
Created April 14, 2018 19:46
Numbers from just measuring the static "number of instructions"

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)