JIT 정수 최적화 피폴(peephole) 규칙 DSL¶

JIT의 정수 핍홀 최적화(peephole optimizations)를 위해, 우리는 정수 연산(들)의 시퀀스를 어떻게 단순화해야 하는지를 명시하는, 패턴 매칭에 기반한 도메인 특화 언어(DSL)를 사용합니다. 이는 jit/metainterp/optimizeopt 디렉터리에 구현되어 있습니다. 이 디렉터리에는 optimizeopt에서 정수 재작성(rewrite)을 위한 DSL의 구현이 들어 있습니다. 그런 다음 이 규칙들은 optimizeopt에서 변환을 실행하는 RPython 코드로 컴파일됩니다. 재작성 규칙은 빌드 프로세스의 일부로 Z3를 사용해 자동으로 정확성이 증명됩니다. 이 페이지는 해당 DSL이 어떻게 작동하는지, 그리고 이를 어떻게 사용하는지에 대한 소개입니다.

단순 변환 규칙¶

DSL의 규칙들은 정수 연산을 어떻게 더 저렴한 다른 정수 연산으로 변환할 수 있는지 명시합니다. 규칙은 항상 이름, 패턴, 대상으로 구성됩니다. 다음은 간단한 규칙입니다:

add_zero: int_add(x, 0)
    => x

규칙의 이름은 add_zero입니다. 이 규칙은 트레이스에서 int_add(x, 0) 형태의 연산과 일치하며, 여기서 x는 무엇이든 일치하고 0은 상수 0에만 일치합니다. => 화살표 뒤에는 재작성의 대상, 즉 해당 연산이 무엇으로 재작성되는지가 오며, 이 경우에는 x입니다.

규칙 언어는 어떤 연산이 교환 가능한지 알고 있으므로, add_zero도 int_add(0, x)를 x로 최적화합니다.

패턴 안의 변수는 반복될 수 있습니다:

sub_x_x: int_sub(x, x)
    => 0

이 규칙은 두 인자가 같은 경우(같은 박스이거나 같은 상수인 경우) int_sub 연산에 대해 매칭됩니다.

더 복잡한 패턴을 가진 규칙은 다음과 같습니다:

sub_add: int_sub(int_add(x, y), y)
    => x

이 패턴은 첫 번째 인자가 int_add 연산으로 생성된 int_sub 연산과 일치합니다. 또한, 덧셈의 인자 중 하나는 뺄셈의 두 번째 인자와 같아야 합니다.

상수 MININT, MAXINT, LONG_BIT(32 또는 64 중 하나입니다)는 규칙에서 사용할 수 있으며, 숫자를 직접 쓰는 것처럼 동작하지만 비트 폭에 독립적인 형식화를 가능하게 합니다:

is_true_and_minint: int_is_true(int_and(x, MININT))
    => int_lt(x, 0)

어떤 상수인지 명시하지 않고 일부 인자가 상수여야 하는 패턴을 사용하는 것도 가능합니다. 이러한 패턴은 다음과 같이 생겼습니다:

sub_add_consts: int_sub(int_add(x, C1), C2) # incomplete
    # more goes here
    => int_sub(x, C)

패턴에서 C로 시작하는 변수는 상수에만 매치됩니다. 하지만 현재 이 형태로는 대상 연산에서 사용되는 변수 C가 어디에도 정의되어 있지 않기 때문에 규칙이 불완전합니다. 이를 계산하는 방법은 다음 절에서 살펴보겠습니다.

상수 및 기타 중간 결과 계산¶

경우에 따라 대상 연산에서 사용되는 중간 결과를 계산해야 할 필요가 있습니다. 이를 위해 규칙 헤드와 규칙 대상 사이에 추가 할당이 있을 수 있습니다.:

sub_add_consts: int_sub(int_add(x, C1), C2) # incomplete
    C = C1 + C1
    => int_sub(x, C)

이러한 대입문의 우변은 Python 문법의 부분 집합으로서, +, -, *를 사용하는 산술 연산과 특정 헬퍼 함수를 지원합니다. 그러나 이 문법을 사용하면 일부 연산에 대해 부호 없음(unsignedness)을 명시적으로 나타낼 수 있습니다. 예를 들어, 부호 없는 오른쪽 시프트에는 >>u가 존재합니다(비교 연산에는 >u, >=u, <u, <=u를 추가할 계획입니다).

검사¶

일부 재작성은 특정 조건에서만 참입니다. 예를 들어, x가 불리언 값을 저장한다고 알려져 있다면, int_eq(x, 1)은 x로 재작성될 수 있습니다. 이는 검사로 표현될 수 있습니다.:

eq_one: int_eq(x, 1)
    check x.is_bool()
    => x

검사(check) 다음에는 불리언 표현식이 옵니다. 패턴에서 가져온 변수는 검사(그리고 대입에서도)에서 IntBound 인스턴스로 사용되어, 추상 해석(abstract interpretation)이 트레이스 변수의 값에 대해 알고 있는 바를 알아낼 수 있습니다.

또 다른 예시입니다:

mul_lshift: int_mul(x, int_lshift(1, y))
    check y.known_ge_const(0) and y.known_le_const(LONG_BIT)
    => int_lshift(x, y)

이는 x * (1 << y)를 x << y로 다시 쓸 수 있음을 표현하지만, y가 0과 LONG_BIT 사이에 있다고 알려져 있는지 확인합니다.

검사와 할당은 반복하거나 서로 조합할 수 있습니다:

mul_pow2_const: int_mul(x, C)
    check C > 0 and C & (C - 1) == 0
    shift = highest_bit(C)
    => int_lshift(x, shift)

IntBound 인스턴스의 메서드를 호출하는 것 외에도, 다음 규칙에서처럼 해당 속성에 접근하는 것도 가능합니다:

and_x_c_in_range: int_and(x, C)
    check x.lower >= 0 and x.upper <= C & ~(C + 1)
    => x

규칙 순서와 생존성(Liveness)¶

생성된 옵티마이저 코드는 재작성 결과로 상수나 변수를 산출하는 규칙을 우선적으로 적용합니다. 이들 중 일치하는 것이 없을 때만 새로운 결과 연산을 산출하는 규칙이 적용됩니다. 예를 들어, sub_x_x와 sub_add 규칙은 sub_add_consts를 시도하기 전에 시도되는데, 앞의 두 규칙은 각각 상수와 변수로 최적화되는 반면, 뒤의 규칙은 결과로 새로운 연산을 산출하기 때문입니다.

규칙 sub_add_consts에는 잠재적인 문제가 있는데, 규칙 헤드에 있는 int_add 연산의 중간 결과가 다른 연산에서 사용되는 경우 sub_add_consts 규칙이 실제로는 연산 수를 줄이지 못한다는 것입니다(그리고 레지스터 압박이 증가하여 오히려 상황을 약간 악화시킬 수도 있습니다). 하지만 현재로서는 JIT의 최적화 패스에서 그런 정보를 고려하기가 극히 어려우므로, 우리는 낙관적으로 그 규칙들을 적용합니다.

규칙 커버리지 확인¶

모든 재작성 규칙(rewrite rule)에는 그것이 실행되는 단위 테스트가 적어도 하나 있어야 합니다. 이를 보장하기 위해, test_optimizeintbound.py 파일의 테스트들은 테스트 실행이 끝날 때 모든 규칙이 적어도 한 번은 실행되었는지 확인하는 assert를 포함하고 있습니다 (이 검사는 예를 들어 -k 옵션으로 개별 테스트를 실행할 때처럼 거짓 양성(false positive)을 일으킬 수 있습니다).

규칙 통계 출력¶

JIT은 jit-intbounds-stats 로깅 범주에서 어떤 규칙이 얼마나 자주 발동했는지에 대한 통계를 출력할 수 있습니다. 예를 들어, 프로그램 실행이 끝날 때 이를 표준 출력(stdout)으로 출력하려면 PyPy를 다음과 같이 실행하십시오.:

PYPYLOG=jit-intbounds-stats:- pypy ...

이 명령의 출력은 대략 다음과 같습니다:

int_add
    add_reassoc_consts 2514
    add_zero 107008
int_sub
    sub_zero 31519
    sub_from_zero 523
    sub_x_x 3153
    sub_add_consts 159
    sub_add 55
    sub_sub_x_c_c 1752
    sub_sub_c_x_c 0
    sub_xor_x_y_y 0
    sub_or_x_y_y 0
int_mul
    mul_zero 0
    mul_one 110
    mul_minus_one 0
    mul_pow2_const 1456
    mul_lshift 0
...

종료와 합류성(Termination and Confluence)¶

현재로서는 안타깝게도 규칙이 실제로 연산을 더 “단순한” 형태로 재작성하는지 확인하는 검사가 없습니다. 비용 모델도 없고, 다음과 같은 규칙을 작성하지 못하게 막는 장치도 없습니다:

neg_complication: int_neg(x) # leads to infinite rewrites
    => int_mul(-1, x)

이렇게 하면, -1을 곱하는 것을 부정(negation)으로 바꾸는 또 다른 규칙이 존재할 경우 끝없는 재작성으로 이어지게 됩니다.

또한 confluence에 대한 검사도 아직 없습니다(아직?). 즉, 규칙이 어떤 순서로 적용되더라도 동일한 입력 트레이스에서 시작하는 모든 재작성이 항상 동일한 출력 트레이스로 이어진다는 속성입니다.

증명¶

모든 코너 케이스에서 항상 올바르지는 않은 피프홀(peephole) 규칙을 작성하기는 매우 쉽습니다. 따라서 기본적으로 모든 규칙은 실제 JIT 코드로 컴파일되기 전에 Z3로 올바름이 증명됩니다. 증명이 실패하면 (바라건대 최소한의) 반례가 출력됩니다. 반례는 검사를 만족하는 모든 입력에 대한 값들, 중간 표현식에 대한 값들, 그리고 소스 연산과 대상 연산에 대한 다른 두 값으로 구성됩니다.

예를 들어, 잘못된 규칙을 추가하려고 하면:

mul_is_add: int_mul(a, b)
    => int_add(a, b)

다음과 같은 반례를 출력으로 얻습니다.:

Could not prove correctness of rule 'mul_is_add'
in line 1
counterexample given by Z3:
counterexample values:
a: 0
b: 1
operation int_mul(a, b) with Z3 formula a*b
has counterexample result vale: 0
BUT
target expression: int_add(a, b) with Z3 formula a + b
has counterexample value: 1

조건을 추가하면, 이는 고려됩니다.:

mul_is_add: int_mul(a, b)
    check a.known_gt_const(1) and b.known_gt_const(2)
    => int_add(a, b)

이는 다음과 같은 반례로 이어집니다:

Could not prove correctness of rule 'mul_is_add'
in line 46
counterexample given by Z3:
counterexample values:
a: 2
b: 3
operation int_mul(a, b) with Z3 formula a*b
has counterexample result vale: 6
BUT
target expression: int_add(a, b) with Z3 formula a + b
has counterexample value: 5

일부 IntBound 메서드는 너무 복잡한 제어 흐름을 갖고 있기 때문에 Z3 증명에 사용할 수 없습니다. 그런 경우, test_z3intbound.Z3IntBound 클래스에 Z3 등가 정식화를 정의할 수 있습니다(이렇게 하는 모든 경우, Z3 친화적인 재정식화와 실제 구현이 서로 다르면 잠재적인 증명 구멍이 될 수 있으므로, 둘이 동등함을 매우 확실히 하기 위해 각별한 주의가 필요합니다).

그것마저 너무 어렵다면, 개별 규칙의 본문에 SORRY_Z3을 추가하여 증명을 건너뛰는 것도 가능합니다(다만 이를 너무 자주 하지 않도록 노력해야 합니다).:

eq_different_knownbits: int_eq(x, y)
    SORRY_Z3
    check x.known_ne(y)
    => 0

충족 가능성 확인¶

규칙이 올바른 최적화를 만들어내는지 확인하는 것 외에도, 해당 규칙이 실제로 적용될 수 있는지도 확인합니다. 이는 규칙의 모든 검사를 충족하는 런타임 값이 일부라도 존재함을 보장합니다. 다음은 이를 위반하는 규칙의 예시입니다.:

never_applies: int_is_true(x)
    check x.known_lt_const(0) and x.known_gt_const(0) # impossible condition, always False
    => x

현재로서는 오류 메시지가 완전히 이해하기 쉽지는 않으며, 이를 나중에 개선하고자 합니다.:

Rule 'never_applies' cannot ever apply
in line 1
Z3 did not manage to find values for variables x such that the following condition becomes True:
And(x <= x_upper,
    x_lower <= x,
    If(x_upper < 0, x_lower > 0, x_upper < 0))

새 규칙 추가하기¶

새 규칙을 추가하려면 (이상적으로는 실제 트레이스에서 관찰된 문제에 기반하여), 다음 단계를 수행해야 합니다:

test_optimizeintbound.py에 실패하는 테스트를 추가하십시오.
규칙을 real.rules에 추가하십시오.
pypy ruleopt/generate.py를 실행하여 Python 코드를 재생성하십시오(이를 위해서는 z3-solver와 rply 패키지가 설치되어 있어야 합니다).
test_optimizeintbound.py가 통과하는지 확인한 다음, 나머지 optimizeopt/ 테스트를 실행하십시오(특히 optimizeopt/test/test_z3checktests.py는 연산과 예상 출력이 타당한지 검사합니다).

DSL 구현 노트¶

DSL의 구현은 비교적 임기응변적인 방식으로 이루어집니다. rply를 사용해 파싱하며, 규칙이 작성된 방식에서 흔히 발생하는 문제를 찾아내려는 작은 타입 검사기가 있습니다. Z3는 Python API를 통해 사용됩니다. 패턴 매칭 RPython 코드는 Luc Maranget의 논문 Compiling Pattern Matching to Good Decision Trees에서 영감을 받은 접근법을 사용해 생성되며, 이해하기 쉬운 소개는 this blog post를 참고하십시오.