17검증 문제

현재 티켓 번호 발급하기

1. 문제와 계약

Ticket.take는 하나의 원자적 트랜잭션에서 두 계약을 함께 만족해야 합니다. 호출자에게는 현재 next에 저장된 번호를 반환하고, 레지스터에는 다음 번호를 예약합니다. starter는 상태 갱신은 올바르게 수행하지만 다음 번호를 반환값으로도 사용합니다. 그래서 공개 실행의 발급 순서가 1이 아니라 십진수 2, 3, 4가 됩니다.

수정 범위는 mkTicket 안의 잘못된 동작입니다. take의 ActionValue method 타입과 상태 갱신, 제공된 최상위 모듈은 그대로 두세요. 현재 반환값과 다음 사이클의 저장값을 같은 값으로 취급하면 안 됩니다.

2. Starter 읽기와 트랜잭션 추적

starter/Main.bsv를 다음 순서로 읽어 보세요.

1. interface Ticket에서 take의 반환 타입과 nextValue의 반환 타입을 비교합니다.
2. next 레지스터의 초기 상태를 확인합니다.
3. take 본문에서 예약된 쓰기와 반환 식의 역할을 따로 표시합니다.
4. issue rule의 <-가 각 호출의 반환값을 결합하는 과정을 확인합니다.
5. 수정하기 전에 매 호출의 (발급값, 다음 저장값)을 예측합니다.

첫 호출이 시작될 때 next는 1입니다. <=는 다음 사이클에 보일 2를 예약합니다. 같은 원자적 Action 안에서 next를 다시 읽어도 여전히 1입니다. return이 <=보다 뒤에 적혀 있어도 새 레지스터 값을 읽지 않습니다. 올바른 상태 추적은 (1, 2), (2, 3), (3, 4)로 이어집니다. 최소 수정은 이미 올바른 상태 전이를 유지하고, 트랜잭션의 반환값을 고르는 식만 계약에 맞춥니다.

수정한 뒤 공개 실행의 발급 순서는 십진수 1부터 빈 번호 없이 증가해야 합니다. 각 호출 뒤의 저장값도 발급값보다 하나 커야 합니다. 출력만 맞추면서 레지스터 갱신을 제거한 코드는 완료 조건을 만족하지 않습니다.

3. 단계별 힌트

4. 추가 실험

필수 수정을 마친 뒤 next의 초기값을 8'hfe로 바꾸고, 세 번 호출할 때의 발급값을 먼저 예측해 보세요. 호출 뒤의 저장값과 8비트 최댓값 다음에 0으로 돌아가는 동작도 함께 추적합니다. 초기값 1 근처가 아닌 폭 경계에서도 같은 ActionValue method 계약이 유지되어야 합니다.