solidity中的SMT（1）

Solidity实现了一种基于SMT（Satisfiability Modulo Theories）和Horn逻辑的形式化验证方法。

2022-06-13

程序语言形式化

SMT formula

Runtime feedback in a meta-tracing JIT for efficient dynamic languages

ECOOP2011，meta-tracing jit通过运行时信息优化object model，核心在于promotion实现的constant fold和operation fold，以及它们的结合体。

2022-02-28

paper阅读

optimization compiler

The Impact of Meta-Tracing on VM Design and Implementation

来自SCP2015，相对详细说明了PyPy JIT优化的一些设计。不过缺少Runtime信息的辅助，留到Runtime feedback in a meta-tracing那篇。

2022-02-24

paper阅读

optimization compiler

Tracing the meta-level:\ PyPy's tracing JIT compiler

ECOOP09，PyPy JIT设计的第一篇，某种意义上算是meta-tracing的开山之作！？（大概，不是很确定）

2022-02-20

paper阅读

optimization compiler

Rethinking Incremental and Parallel Pointer Analysis

Rethinking Incremental and Parallel Pointer Analysis来自TOPLAS，介绍了一种增量的可并行的指针分析算法。

2022-02-13

paper阅读

static analysis

CPython Key-Sharing Dictionary优化

聊一下所知道的cpython dict结构的优化工作

2022-01-16

Python

optimization CPython

Lazy Basic Block Versioning续

Interprocedural Type Specialization of JavaScript Programs Without Type Analysis 来自ECOOP2016，是在Simple and Effective Type Check Removal through Lazy Basic Block Versioning基础上实现的，主要将BBV扩展到interprocedura

2022-01-13

paper阅读

optimization compiler

Lazy Basic Block Versioning

Simple and Effective Type Check Removal through Lazy Basic Block Versioning，这篇论文来自ECOOP2015，介绍了一种可以有效消除类型检查的技术，用于动态类型语言的JIT编译。

2022-01-03

paper阅读

type system optimization

Functional programming compiler optimization

Can a functional programming language compiler optimize as well as an imperative programming language compiler in practice?在搜索FP优化的时候看到这么一个问题

2021-12-31

PL

optimization

Is sound gradual typing dead 解读

Is sound gradual typing dead? 主要研究sound gradual typing在编译中的收益问题，结论认为通过gradual type来指导编译优化是一件不划算的事情。简介动态类型语言在构建（或者生长）出复杂软件系统的时候会因为缺少可靠的类型信息而变得难以维护。一种解决方法是通过扩展语言，增量的增加类型信息。Gradual typing就是通过type annota

2021-12-01

paper阅读

type system

Blog复活辣

Blog重建计划表

2021-11-29

胡言乱语

费力的dex字节码转换器

闲话三个多月磨磨唧唧，终于拿出了一版稍微有那么点样的开源工具–dedx。链接https://github.com/penguin-wwy/dedx

2019-12-05

Open Source Project

jvm bytecode