19구현 문제
두 레지스터를 원자적으로 교환하기
1. 문제와 수정 범위
update rule은 현재의 4비트 값 두 개를 한 번만 교환해야 합니다. Starter의 두 대입은
각 레지스터 값을 같은 레지스터에 다시 저장합니다. 따라서 start를 호출해도 공개
실행에서 초기 값 쌍이 그대로 남습니다.
수정 범위는 TODO 아래의 대입문 두 개입니다. 인터페이스, ready condition, started
protocol, mkTop은 그대로 두세요. 초기값뿐 아니라 load로 전달되는 모든 값 쌍에서 같은
동작이 성립해야 합니다.
2. Starter 읽기
Starter는 다음 순서로 읽어 보세요.
| 순서 | 확인할 선언 | 판단할 내용 |
|---|---|---|
| 1 | AtomicPair | 호출자가 상태를 넣고 실행하며 결과를 읽는 방법 |
| 2 | leftReg, rightReg, started | 값 쌍과 실행 가능 상태를 저장하는 위치 |
| 3 | update | started가 참일 때 계산하는 next-state 값 |
| 4 | load, start | 실행 대기 중에 새 요청을 허용하지 않는 조건 |
| 5 | mkTop | 요청 사이클과 최종 관찰 사이의 간격 |
수정하기 전에는 start가 commit된 다음 사이클에 update가 활성화됩니다. 자기 자신을
다시 쓰는 대입문은 진입 상태의 값을 같은 레지스터에 저장합니다. 이후 사이클에도 두 값은
바뀌지 않습니다. 실행 전에 이 동작을 먼저 예측해 보세요.
3. 최소 수정의 근거
두 목적지의 next-state 값이 어느 레지스터에서 와야 하는지만 바꾸세요. 한 rule의 모든
오른쪽 식은 같은 진입 상태를 읽습니다. 소프트웨어식 교환을 흉내 내는 임시 레지스터나
추가 단계는 필요하지 않습니다. 대입문 순서를 바꿔도 둘째 오른쪽 식이 읽는 값은 달라지지
않습니다.
완료 여부는 여러 사이클에 걸쳐 판단합니다.
| 관찰 시점 | 만족해야 하는 상태 |
|---|---|
start 전 | 넣은 값 쌍이 안정적으로 유지됩니다. |
update 진입 | 두 레지스터가 교환 전 값을 그대로 가집니다. |
update 완료 에지 | 두 next-state 값이 함께 반영되고 started가 거짓이 됩니다. |
| 이후 사이클 | 교환된 값이 유지되고 다시 교환되지 않습니다. |
같은 값 두 개, 0, 4비트 최댓값에서도 같은 전이가 성립해야 합니다. 공개 출력 한 번만 맞고 한쪽 값이 먼저 바뀌거나 다음 사이클에 재실행되면 완료가 아닙니다.
4. 단계형 힌트
힌트 1 — 상태 전이
update 진입 시점의 값 쌍과 완료 에지 뒤의 값 쌍을 먼저 표로 적어 보세요. 오른쪽 식을
평가하는 동안에는 레지스터 값이 바뀌지 않습니다.
힌트 2 — 수정 위치
계약을 위반하는 선언은 TODO 아래의 자기 대입 두 개뿐입니다.
started <= False는 한 번만 실행되게 만드는 올바른 대입입니다.
힌트 3 — 값의 출처
각 목적지는 진입 상태에서 반대편 레지스터가 가진 값을 받아야 합니다. 각 레지스터 읽기를 한 번씩 사용하고, 순차 제어는 추가하지 마세요.
5. 추가 실험
필수 수정을 마친 뒤 초기 값 쌍을 같은 값 두 개로 바꾸고 다시 실행해 보세요. 값만 보고는 교환 여부를 구분할 수 없는 이유를 설명해 보세요. 이어서 0과 4비트 최댓값을 사용해, 한쪽만 바뀌거나 같은 레지스터를 두 번 읽는 오류가 어떻게 드러나는지 예측해 보세요. 추가 실험은 채점 조건이 아닙니다.