행렬(서로 다른 속성들의 교차 필요)과 같은 연산 처리로 DAG 를 만들자 - 아이디어 정리

1. 아이디어의 정체

핵심 개념 묶음

• Abstract Interpretation (추상 해석)
  • 프로그램을 실행하지 않고
  • 값 대신 속성 / 제약의 요약 상태를 흘려보냄
  • DAG 위에서 상태를 누적, 교차
• Attribute Algebra / Constraint Composition
  • 각 노드는 속성 벡터를 가짐
  • 합성 시 단순 merge 가 아니라 교차 검사
  • 불가능하면 invalid
• Effect / Capability System (확장형)
  • 이 연산은 무엇을 요구하고, 무엇을 보장하는가
  • 누적되며 제약이 강화됨

이 셋이 같은 철학의 다른 표현

 

2. 행렬 표현을 이론 언어로 번역하면

각기 다른 행들이 서로 다른 정보를 가지고 있고, 이 성분들의 교차 적용 누적의 표현

컴파일러 용어로

Abstract State Vector + Join / Compose Operator

 

처음 상상한 구조

[ shape     ]
[ dtype     ]
[ layout    ]
[ epilogue  ]
[ memory    ]
[ sidefx    ]

• 각 row = 서로 다른 속성 공간
• op 마다 이 행렬이 하나씩 있음
• 누적 시 교차 검사 발생

 

기존 이론에서의 대응

• 행렬의 각 행 : Attribute / Abstract Domain
• 행렬 누적     : Abstract State Propagation
• 성분 교차     : Constraint Join / Meet
• 불가능 상태  : Bottom
• 최종 행렬    : Fixed-point Abstact State
• DAG 내포   : Control / Data-flow sensitivity

 

왜 행렬 곱 같은 느낌이 드는지

• 단순 덧셈이 아닌
• 성분 간 상호작용이 있음
• 결과가 입력보다 더 많은 의미를 가짐

수학적으로

Semiring / Lattice 위의 합성 연산

• join = 가능성의 합
• meet = 제약의 교차

이라는 점에서 행렬 곱 비유

 

완성된 행렬이 DAG 특성을 가진다는 말에 대해

• Abstract State 는
  • DAG 의 모든 경로 제약을
  • 요약한 결과

그래프를 들고 있는 것이 아닌, 그래프에서 유도된 제약의 집합을 들고 있음

 

완성된 state 하나가 DAG 전체의 실행 가능성 공간을 압축표현

이것이 Abstract Interpretation 의 핵심 목표