gterzian: The current implementation seems to only process one image at a time, while the spec allows more than one image to be in the key, with the goal of generating keys in batches of more than one(on occasion).
If you agree that the spec allows for this, please change the logic accordingly.
GitHub Copilot: You are correct. The current implementation only ever puts one image into the PendingKey
state at a time because the StartLoad
action is only performed for a single image before the thread waits. This prevents the system from ever requesting a batch of more than one key, which defeats the purpose of the batching logic in the specification.
I have updated the code to allow a thread to perform multiple StartLoad
actions in a single turn. This will allow multiple images to enter the PendingKey
state, enabling the system to generate key batches as intended by the spec.
// ...existing code...
if !action_taken {
// \E i \in Image
// Note: To allow for batching, a thread can perform multiple StartLoad
// actions in one turn. This allows multiple images to be in the
// PendingKey state, so that key generation can happen in batches.
for &image in images_clone.iter() {
// StartLoad(i)
// /\ image_states[i] = "None"
if *guard.image_states.get(&image).unwrap() == ImageState::None {
// /\ image_states' = [image_states EXCEPT ![i] = "PendingKey"]
guard.image_states.insert(image, ImageState::PendingKey);
// /\ image_queue' = Append(image_queue, i)
guard.image_queue.push_back(image);
action_taken = true;
}
}
}
}
if action_taken {
// ...existing code...