라이브 코딩 언어를 위한 시간 의미론 [pdf]

• 교육용 라이브 코딩 언어인 소닉 파이(Sonic Pi)의 시간 의미론(Temporal Semantics) 구조와 발전 과정을 상세히 분석함.
• 초기 버전(v1.0)의 순차적 실행 시간에 의존한 sleep 함수가 유발하는 타이밍 드리프트(Drift)와 지터(Jitter) 문제를 규명함.
• 가상 시간(Virtual Time)과 실제 시간(Real Time)의 상호작용을 통한 새로운 sleep 의미론(v2.0)을 제안하고, 이를 모나드(Monad) 모델 및 시간 시스템(Time System)으로 정형화하여 시간적 안전성(Time Safety)을 증명함.

---

서론 (Introduction)

• 음악에 있어 타이밍은 필수불가결한 요소이며, 소리가 정확한 시간에 재생되는 것은 컴퓨팅 관점에서 중대한 요구사항임.
  • 기존의 '실시간 컴퓨팅(Real-time computing)'은 주로 정해진 기한(Deadline) 내에 작업을 완료하여 성능을 높이는 데 초점을 맞춤.
  • 반면 음악이나 로봇 보행 같은 기계적 조정 작업에서는 너무 이른 것(Early)도 너무 늦은 것(Late)만큼이나 치명적이므로, 고도로 정확하고 견고한 타이밍 모델이 필요함.
• 소닉 파이(Sonic Pi)는 음악 라이브 코딩(Live coding)을 통해 학생들에게 컴퓨팅 개념을 가르치기 위해 설계된 도메인 특화 언어(DSL)임.
  • 대부분 순수 함수형 성격을 띠지만, 소리 출력과 타이밍 조절이라는 부수 효과(Effects)에서 비순수성(Impurity)이 발생함.
• 논문의 주요 기여 세 가지는 다음과 같음.
  • 효과의 정확한 타이밍 제어를 위해 이전 버전과 문법적 호환성을 유지하면서도 완전히 개선된 프로그래밍 접근법(v2.0) 도입.
  • 소닉 파이 프로그램의 시간적 동작에 대한 정적 분석(Static analysis)을 제공하는 공리적 추상 모델인 '시간 시스템(Time system)' 정립.
  • 핵심 하위 언어에 대한 모나딕 표시 의미론(Monadic denotational semantics)을 제시하고, 시간 시스템의 기준에 부합하는 '시간적 안전성(Time safety)' 증명.

소닉 파이 v1.0의 타이밍 문제 (Problems with timing in Sonic Pi v1.0)

• 소닉 파이 v1.0은 영국 컴퓨팅 교육 과정의 핵심인 '명령어의 순차적 실행(Sequential ordering of effects)'을 직관적으로 시연하는 데 초점을 맞추었음.
  • 빠른 프로세서 속도를 이용해 명령어가 연속으로 실행되면 사용자가 이를 하나의 화음처럼 인식한다고 전제함.
  • 각 소리 간에 간격을 두기 위해 POSIX의 전통적인 sleep 함수와 유사하게 일정 시간 동안 스레드의 연산을 정지하는 방식을 사용함.
• 문제점 1: 연산 시간 누적에 의한 심각한 타이밍 드리프트(Drift) 현상 발생.
  • 각 명령어 연산 시간($\Delta$)과 스케줄러가 스레드를 다시 활성화하는 데 걸리는 시간 등이 sleep 시간에 합산됨.
  • 이로 인해 프로그램의 실제 경과 시간은 명시된 박자 수식보다 점진적으로 길어지며 리듬이 어긋남.
  • 예시: 여러 스레드가 동시에 실행될 경우, 스레드별 연산 비용 차이로 인해 초반 동기화가 무너지고 제각각의 속도로 표류하게 됨.
• 문제점 2: 비동기 메시지 지연에 따른 지터(Jitter) 현상 발생.
  • 소리 재생(play)이나 샘플 재생(sample) 명령은 외부 신디사이저 프로세스로 보내지는 비동기 메시지이므로, 메시지 전송 및 해석 과정에서 가변적인 시간 오차가 추가됨.
• 수학적 요약: 기존 버전에서의 총 실행 시간은 $\Delta_{a}+\Delta_{b}+\Delta_{c}+1+\Delta_{d}+\Delta_{e}+\Delta_{f}+0.5+\Delta_{g}+\Delta_{h}+\Delta_{i}$ 와 같이 각 코드 블록의 불확실한 소요 시간이 누적되는 구조임.

Sleep의 재발명 / v2.0 개선안 (Reinventing sleep)

• v2.0은 사용자(특히 비전문 음악가)의 '암묵적인 음악적 기대(Implicit rhythmical expectations)'를 충족하기 위해 sleep의 의미론을 새롭게 재정의함.
• 새로운 프로그래밍 모델은 효과의 '순서(Ordering)'와 '타이밍(Timing)'을 명확히 분리함.
  • sleep t는 단순히 t초 동안 멈추는 것이 아니라, "직전의 sleep 이후 최소 t초가 경과될 때까지 연산을 차단하는 시간적 장벽(Temporal barrier)" 역할을 수행함.
• 가상 시간(Virtual Time)의 도입.
  • 오로지 sleep 연산에 의해서만 증가하는 스레드 로컬(Thread-local) 가상 시간 변수를 운용함.
  • 시스템은 다음 sleep 호출 시, 이전 연산들에 소모된 실제 시간을 파악하여 요청된 sleep 시간에서 그 오차를 미리 차감함.
  • 예시: sleep 1 명령 수행 시 이미 0.1초가 앞선 연산에 소비되었다면 0.9초만 대기하므로 시간 누적(Drift)이 원천 차단됨.
• 스케줄 어헤드 타임(ScheduleAheadTime) 도입.
  • $\Delta$ 연산 시간과 서버로 메시지를 전송하는 지터를 상쇄하기 위해, 외부 효과 스케줄링 시 가상 시간에 일정한 상수 값을 추가해 오차를 덮음.
• 연성 기한(Soft deadline)과 안전 매커니즘.
  • 연산 시간이 지정된 대기 시간을 심각하게 초과할 경우 하드 데드라인(Hard deadline)을 강제하지 않고 오버런 경고를 발생시킴.
  • 일정 허용치를 벗어나 무한 반복 등 자원 고갈 위험이 생기면 시간 예외(Time exception)를 던져 스레드를 자가 종료시킴.

소닉 파이를 위한 시간 시스템 (A time system for Sonic Pi)

• 프로그램의 시간적 동작을 규정하는 추상적이고 공리적인 '시간 시스템(Time System)'을 명세함.
• 가상 시간($[-]_v$)과 실제 시간($[-]_t$)의 공리 정의.
  • 가상 시간: sleep t 연산에 대해서만 $t$ 값만큼 반환하고 증가하며, 그 외의 변수 할당이나 단순 효과(Actions, $A^i$) 연산에서는 0을 반환함.
  • 실제 시간: sleep의 실제 지연 시간은 독립적으로 결정되지 않고, 그 앞단에 존재하는 프로그램 문맥($[P]_t$)의 지연 시간에 종속되어 유동적으로 정해짐.
    • 수학적 정의: $[P; sleep~t]_t = ([P]_v+t) \max [P]_t$.
• 시간에 대한 동치 관계(Equality on time, $\approx$) 정의.
  • 실행 오버헤드와 비결정성에 의한 미세한 오차 $\epsilon$을 감안하여, $s \approx t \equiv |(s-t)| \le \epsilon$ 으로 동치 관계를 상정함.
  • $\epsilon$ 차이가 발생하더라도 앞서 언급한 sleep 장벽 시스템에 의해 이 오차가 다음 주기로 누적되지 않음.
• 보조정리 1 (Lemma 1): $[P]_t \ge [P]_v$.
  • 모든 소닉 파이 프로그램의 실제 실행 시간은 절대로 규정된 가상 시간보다 짧을 수 없음 (Under-run 불가).

시간 의미론의 표시적 모델 (A denotational model of Sonic Pi's temporal semantics)

• 메타 언어인 하스켈(Haskell)을 활용해 소닉 파이의 부수 효과를 캡슐화하는 Temporal 모나드(Monad)를 구축함.
• Temporal 모나드의 작동 원리.
  • 시작 시간(Start time)과 현재 시간(Current time) 쌍을 받아, 가상 시간의 상태를 갱신(Old -> New)하면서 시스템 OS의 시계(IO monad)에 접근하는 구조로 되어 있음.
• sleep 의미론의 표시적 해석.
  • 현재 시간과 새로 목표하는 가상 시간($vT^{\prime}$)을 비교함.
  • 목표 가상 시간이 현재 경과 시간보다 크다면 그 차이만큼만 실제 커널 레벨의 정지(kernelSleep)를 수행하고, 반대의 경우 정지 없이 연산을 이어감.
• 시간적 안전성 증명(Time safety property).
  • 이 모나드 모델의 계산 결과가 기존 공리적 명세(시간 시스템)의 불변성을 모두 충족함을 증명함.
  • 모나드 해석을 거친 코드의 실행 시간 수식 단순화를 통해, 오차 범위 $\epsilon$ 이내에서 안정적으로 동작함을 수학적으로 입증함.
• 모나드 법칙 준수 여부(Equational theory).
  • 실행 과정이 실제 시간(Current time)에 의존하기 때문에 일반적인 모나드 법칙이 성립하지 않는 '약한(Weak)' 모나드임.
  • 그러나 소닉 파이 언어 단에서는 실제 시스템 시간을 유저에게 노출하는 기능이 없기 때문에, 이를 배제하고 해석하면 동치 이론(Equational theory)이 유효하게 작동함.

초과 실행 경고 발생 (Emitting overrun warnings)

• 허용 오차 오버런을 추적하기 위해 기존 모나드를 확장한 TemporalE 구조를 제안함.
• 최대 허용 오버런 값인 $\epsilon$ 파라미터와 경고 로그를 쌓는 출력 스트림(Writer monad 역할)을 결합함.
• 두 가지 수준의 경고 판정.
  • 강한 경고(Strong Warning): 프로그램의 실제 실행 시간이 가상 시간보다 허용 오차 $\epsilon$를 초과하여 앞설 때 발생함 ($[P]_t > [P]_v + \epsilon$).
  • 약한 경고(Weak Warning): 실행 시간이 가상 시간보다는 지연되었으나, 그 차이가 허용 오차 $\epsilon$ 이내일 때 발생함 ($[P]_v \le [P]_t < [P]_v + \epsilon$).

결론 및 시사점 (Conclusion)

• 새롭게 개편된 소닉 파이는 직관적인 구문 호환성(Syntactic compatibility)을 유지하면서도 음악적 예측이 가능한 안정적인 시간 의미론을 제공함.
• 엄밀한 정형 의미론(Formal semantics)을 통해 정의된 '시간적 안전성(Time Safety)' 접근법은 단순한 음악 프로그래밍의 영역을 넘어, 로보틱스나 기타 물리적 세계와 인터랙션하는 시간적 조정(Temporal coordination) 언어로 확장될 높은 잠재력을 시사함.