centril 2017-03-06 11:46:19
johnw, ski so... what does :t Applicative f => (b -> f b) -> a -> f a translate in the lens library if anything ?
wizardwizard 2017-03-06 11:46:24
so what work, if any, has been done on programming languages targeting heterogeneous computing platforms
centril 2017-03-06 11:46:26
translate to *
johnw 2017-03-06 11:46:30
Traversal
wizardwizard 2017-03-06 11:46:36
for example, i might have a computer with a single core CPU as a compilation target
wizardwizard 2017-03-06 11:46:48
while another machine might be a quad core CPU with an FPGA attached
wizardwizard 2017-03-06 11:46:53
and a third might be a dual core CPU with GPU
wizardwizard 2017-03-06 11:47:18
and i might want to compile my program for any of the three platforms and get the best performance
johnw 2017-03-06 11:47:27
Traversal' :)
wizardwizard 2017-03-06 11:47:37
i might also need to provide some kind of formal description of my target platform to inform the compiler,...
centril 2017-03-06 11:48:14
wizardwizard: is the platform specified at compile time?
centril 2017-03-06 11:48:28
i infer that it is
wizardwizard 2017-03-06 11:48:35
ideally my code would know nothing about what platform it is being compiled to
wizardwizard 2017-03-06 11:48:50
but i could have separate code which provides as much detail as you want about the platform
centril 2017-03-06 11:48:51
right, but the compiler does ?
wizardwizard 2017-03-06 11:48:55
cache sizes, etc
peddie 2017-03-06 11:49:01
wizardwizard: have you looked at OpenCL? also, LLVM can generate code for different platforms (e.g. NVIDIA GPUs or intel CPUs) from a subset of its IR
wizardwizard 2017-03-06 11:49:03
the compiler would receive (1) my program and (2) the platform desciption
centril 2017-03-06 11:49:04
then I'd say LLVM
centril 2017-03-06 11:49:21
this is exactly what LLVM does...
wizardwizard 2017-03-06 11:49:39
LLVM opportunistically makes use of the GPU?
centril 2017-03-06 11:50:08
wizardwizard: well... that is a matter of adding optimization passes for that into LLVM, but in principle there should be nothing stopping it
wizardwizard 2017-03-06 11:50:18
i think openCL produces code for single targets
centril 2017-03-06 11:50:19
LLVM already does auto-vectorization, etc.
centril 2017-03-06 11:51:12
the problem with GPUs is that they are very free to change from one iteration to another, and the abstraction-layers are not really meant for general purpose computation, until recently at least
wizardwizard 2017-03-06 11:51:26
right
wizardwizard 2017-03-06 11:51:37
and i can't keep up with heterogeneous architectures
wizardwizard 2017-03-06 11:51:41
it's just not feasible
wizardwizard 2017-03-06 11:51:56
i want to throw my code at a compiler and have it actually figure out what to do
centril 2017-03-06 11:52:06
I guess LLVM could compile to openCL / CUDA, etc... ?
dedgrant 2017-03-06 11:57:11
wizardwizard, centril, reminds me of this PASC project: http://www.pasc-ch.org/projects/projects/heterogeneous-compiler-platform/ (but I have no other info)
peddie 2017-03-06 11:57:23
centril: http://llvm.org/docs/NVPTXUsage.html
wizardwizard 2017-03-06 11:57:41
given that intel is going to start shipping CPUs with integrated FPGAs
wizardwizard 2017-03-06 11:58:22
it would be nice if my code simply automatically made use of whatever compute resource was available
centril 2017-03-06 12:04:17
wizardwizard: yes, wouldn't it be nice if your code just magically ran on the GPU ;)
wizardwizard 2017-03-06 12:04:24
well yeah, that's the point
centril 2017-03-06 12:04:31
unfortunately, someone has to do the work ^^
wizardwizard 2017-03-06 12:04:45
it can't be that hard to pick out vector operations
centril 2017-03-06 12:05:16
well... doing vector opt in CPU is easier because the cost of moving data is less
wizardwizard 2017-03-06 12:05:33
right but in addition to a descrption of the system
centril 2017-03-06 12:05:34
but if you are moving stuff via PCI-E, then the compiler has to consider the cost of moving data to GPU first
wizardwizard 2017-03-06 12:05:42
the compiler could run various benchmarks testing latency, bandwidth, etc
wizardwizard 2017-03-06 12:05:49
and actually reason about the code
wizardwizard 2017-03-06 12:06:00
and even compile it, test perf, tweak, and so on
centril 2017-03-06 12:07:18
you cant write optimizations for a target that is moving too fast
centril 2017-03-06 12:08:17
wizardwizard: another thing on my wishlist: rewrite LLVM in Rust
wizardwizard 2017-03-06 12:08:25
heh why?
wizardwizard 2017-03-06 12:08:32
finding bugs?
centril 2017-03-06 12:08:48
Cause C++ be unsafe
wizardwizard 2017-03-06 12:09:05
because you think LLVM has defects?
wizardwizard 2017-03-06 12:09:24
a minisat rewrite in rust found at least one serious bug
centril 2017-03-06 12:09:37
anything sizeable written in C++ is bound to have defects somewhere
centril 2017-03-06 12:09:49
and I'd very much not like bugs in a compiler...
centril 2017-03-06 12:10:06
I'd say bug free compilers are even more important than bugfree kernels
centril 2017-03-06 12:10:50
mniip: why not Agda? or Idris?
zv 2017-03-06 12:11:00
wizardwizard: even large SAT solvers have huge bugs, SMT solvers doubly so.
wizardwizard 2017-03-06 12:11:27
haha
wizardwizard 2017-03-06 12:11:32
so why use them?
wizardwizard 2017-03-06 12:11:46
i guess,... run on two independent implementations...?
mniip 2017-03-06 12:11:49
they are crazy fust
mniip 2017-03-06 12:11:51
fast*
zv 2017-03-06 12:11:55
sortof
wizardwizard 2017-03-06 12:15:38
you can verify, but what does the verification?
mniip 2017-03-06 12:15:38
otherwise, is there a reason a SAT solver can't benefit from a graph encoding of the input as opposed to a CNF
zv 2017-03-06 12:15:43
That SMTLIB2 code is going to be converted into 700 variables and 1060 clauses
solrize 2017-03-06 12:15:47
mniip, compcert.inria.fr
monochrom 2017-03-06 12:15:52
There is no real loss if an SMT solver is wrong. No real loss compared to the days before there were SMT solvers.
centril 2017-03-06 12:15:54
https://en.wikipedia.org/wiki/Conjunctive_normal_form#Computational_complexity
wizardwizard 2017-03-06 12:16:08
computing is a steaming pile of dung
wizardwizard 2017-03-06 12:16:21
and is impossible to do correctly
wizardwizard 2017-03-06 12:16:23
i think that's the lesson
monochrom 2017-03-06 12:16:44
That is, before, you assumed (wrongly) that your program was perfect.
centril 2017-03-06 12:16:47
wizardwizard: that is a really sad lesson i hope not to draw
centril 2017-03-06 12:17:43
some languages allow computing to be made more correctly
centril 2017-03-06 12:18:18
(Idris/Agda/Haskell/Rust, ...)
monochrom 2017-03-06 12:19:01
With a buggy SMT solver, sometimes it correctly points out a bug, so you gain. Sometimes it incorrectly overlooks a bug, no loss compared to before. Sometimes it incorrectly claims you have a bug, but you will investigate, right? You will find that the bug is not with your program, no loss.
mniip 2017-03-06 12:19:36
centril, yeah but CNF is exponential of the input size
mniip 2017-03-06 12:21:02
so no wonder it's NP-hard timewise
centril 2017-03-06 12:23:40
monochrom: if your compiler claims that correct programs are incorrect then we have a problem...
zv 2017-03-06 12:25:15
mniip: it's possible to immediately eliminate many unprofitable avenues of exploration (in the universe of possible satisfactions of a set of variables), so not nessasarily
centril 2017-03-06 12:25:15
mniip: what about the k-SAT thingy ?
zv 2017-03-06 12:25:15
kSAT is even more complex
centril 2017-03-06 12:25:15
2-SAT then
wizardwizard 2017-03-06 12:25:25
maybe even code => networked devices
wizardwizard 2017-03-06 12:25:32
hehe
centril 2017-03-06 12:25:50
wizardwizard: I claim Code => GPU is a subproblem of your problem
wizardwizard 2017-03-06 12:26:05
yeah :)
koala_man 2017-03-06 12:26:44
centril: neat. what does it handle that testing doesn't?
centril 2017-03-06 12:26:45
reading the JLS is not much fun... at every corner there is another special case
zv 2017-03-06 12:26:52
centril: it's definitely doable at this point
zv 2017-03-06 12:27:33
That is to say, "Making abstract claims about machine code", or perhaps even Java
centril 2017-03-06 12:27:51
koala_man: we use normalization + strategies to verify that 2 programs are the same structurally, instead of running the code
centril 2017-03-06 12:28:12
well... since normalization + strategies is undecidable, we fall back on property based testing
centril 2017-03-06 12:29:20
zv: replicating this in LLVM would be interesting
dedgrant 2017-03-06 12:29:29
wizardwizard: If you rephrase your problem as, "what if we had a solution to the Optimization Problem?" then we could say that SMT solvers have resulted in some powerful tools for exploring the problem.
centril 2017-03-06 12:29:35
then you can prove that 2 programs from 2 diff languages are the same
zv 2017-03-06 12:29:44
centril: have you heard of the tool Klee?
koala_man 2017-03-06 12:30:03
centril: so an exercise would be e.g. "quicksort a list" and not a broader "sort a list"?
zv 2017-03-06 12:32:13
It operates on LLVM IR, can 'symbolically execute' a program without every actually running it
