Optimizing Datalog for the GPU
blakepelton | 115 points
The work done/supervised by Kristopher Micinski on using HPC hardware (not only GPUs but clusters) for formal methods is really encouraging. I hope we reach a breakthrough of affinity between COTS compute hardware and all kinds of formal methods, as GPUs found theirs with deep learning and subsequent large models.
One possible answer to 'what do we do with all the P100s, V100s, A100s when they're decomissionned from their AI heyday (apart from 'small(er) models'.
touisteur | a day ago
Curious, why use cuda and hip? These frameworks are rather opinionated about kernel design, they seem suboptimal for implementing a language runtime when SPIR-V is right there, particularly in the case of datalog.
ux266478 | a day ago
On a side note, what tools that leverage Datalog are in use by the HN crowd?
I know that Datomic[0] is very popular. I've also been playing with Clingo[1] lately.
[0] https://www.datomic.com/
[1] https://potassco.org/clingo/