46검증 문제

잘못된 implicit condition 계약 고치기

1. 문제와 수정 범위

rule의 실행 조건에는 머리에 적은 명시적 조건과, 본문에서 호출한 method의 implicit condition이 모두 들어갑니다. consume은 active를 명시적 조건으로 쓰면서 FIFOF의 first와 deq도 호출합니다. 큐가 비어 있으면 두 method를 쓸 수 없는데, consume 앞의 scheduling 어트리뷰트는 호출한 method가 조건을 더하지 않는다고 선언합니다. 이 모순 때문에 컴파일 오류가 발생합니다.

consume의 scheduling 계약만 수정하세요. 큐 동작, 레지스터 갱신, 인터페이스, mkTop은 그대로 둡니다.

2. starter 읽기와 실행 전 예측

상태와 조건을 나누어 읽어 보세요.

실행 전에 컴파일 결과를 먼저 예측해 보세요. 어트리뷰트는 active만 참이면 consume이 실행될 수 있다고 요구합니다. 하지만 실제 조건은 active가 참이고 큐에 항목이 있다는 두 조건의 논리곱입니다. 이 오류는 scheduling 단계에서 검출됩니다. 시뮬레이션 시간 초과가 아니며, active 조건이 틀렸다는 뜻도 아닙니다.

3. 최소 수정과 완료 조건

컴파일러가 큐 method의 실제 implicit condition을 실행 조건에 남기게 하세요. 명시적 active 조건, first, deq, 레지스터 갱신은 그대로 둡니다. queue.notEmpty를 머리에 덧붙이지도 마세요. 같은 제어를 표현할 수는 있지만, method의 준비 조건이 이미 rule 조건에 들어간다는 점을 가립니다.

consume은 active가 참이고 항목이 있을 때만 실행되어야 합니다. 이 논리곱이 유지되면 빈 큐에서는 rule이 기다리고, 유효하지 않은 읽기나 꺼내기를 하지 않습니다.

수정한 뒤 실행은 컴파일에 성공하고 result = 7c를 출력해야 합니다. 그 과정은 다음 순서를 따릅니다. fill이 바이트를 넣고, start가 active를 세우고, consume이 같은 바이트를 resultReg에 반영하면서 doneReg를 참으로 만듭니다. show는 done이 참이 된 뒤에만 결과를 읽습니다. 빈 큐에서 start가 먼저 실행되어도 consume은 기다리다가 값이 들어온 뒤에 실행되어야 합니다. 공개 실행의 값 하나만 저장하는 구현은 완료 조건을 만족하지 못합니다.

4. 단계형 힌트

5. 추가 실험

수정을 마친 뒤 별도 사본에서 start가 fill보다 먼저 실행되도록 순서를 바꿔 보세요. 어느 rule이 기다리는지, 값을 넣은 뒤 어떤 implicit condition이 바뀌는지, 빈 큐에서 꺼내기가 일어나지 않는 이유를 예측해 보세요. 채점 대상이 아니므로 제출하기 전에 되돌리세요.