1. Introduction
It's always hard to write code for parallel programs, and harder to write correct and fast code on GPU. Writing a simple CUDA Renderer would be an opportunity to practice.
SMT-可满足性模理论
Posted on
In
PL
SMT Solver
继上篇有关 SAT 的介绍，我们接着展开看看 SMT - Satisfiability Modulo Theories。 SAT 是基于布尔逻辑回答某个命题的可满足性，如\(x \vee y\)。但现实中有各种其他的理论， 如实数理论等：\(a < c \vee a > b\)，那我们怎么判断这种公式的可满足性呢？
SAT-布尔可满足性理论
Posted on
In
PL
什么是约束求解？
现实世界中有许多问题可以被抽象为基于约束(Constraint)的问题，约束指的是就是条件。
而约束求解就是在给定约束的情况下，如果可满足(Satisfiable)我们就返回一组解， 如果不可满足，我们就给出一个较小的矛盾集(Unsatisfiable core)。
线性代数的小trick-0
Posted on
In
Linear Algebra
矩阵多项式
对于矩阵\(A\)，我们假设有关于矩阵\(A\)的\(n\)次多项式 \(f(A) = c_nA^n+c_{n-1}A^{n-1}+\cdots+c_1A+c_0E\)
那么假设我们知道\(A\)的特征值\(\lambda_1,\lambda_2, \cdots, \lambda_n\)
那么\(f(A)\)的特征值会是什么呢？
Introduction to GPU
Introduction
GPU, Graphics Processing Unit, is initially designed to accelerate image rendering such as video games. For its high performance at parallel computation, it has become a great processor for accelerating DL/ML training.
有关LLVM的文档
Looking into ELF Symbol Table
Introduction
ELF, Executable and Linking Format (ELF) files, is a universal binary format in Linux. As its name suggests, any executable or linking files in Linux are in format of ELF, which consists of an ELF header, followed by a program header table or a section header table, or both. The two tables describe the rest of the particularities of the file.
The header file <elf.h> defines the format of ELF files and related C structures.
(Paper Reading) SCC-Based Value Numbering
Introduction
Value Numbering is a universally useful optimization implemented by most compilers like Clang, GCC, etc. Traditionally GVN can be divided into Hash-Based and Value-Partitioning. The former handles algebraic simplifications but locally. The latter is global but handling only simple redundancies. K. C and T. S came up with a new method to solve it for SSA.
How to debug LLVM ?
Abstract
Debugging programs remains a significant topic in software engineering field. Especially in system software like Compiler, it's difficult to pinpoint the root and solve relative problems.
For my recent work on LLVM, I'd like to share some experience about it.
LLVM源码解析- EarlyCSE
Abstract
Common sub-expression elimination (CSE) is an important optimization for compilers, which is similar to partial redundancies elimination optimization.
CSE is designed to eliminate those expressions with identical and semantically equivalent components, with consideration for some properties like commutativity, associativity of operators.
For LLVM, there is EarlyCSE pass as one of implementation for CSE. The "Early" in EarlyCSE means that simple, fast and can be applied in every stages it needs.