Skip to content

Instantly share code, notes, and snippets.

@gterzian
Created July 1, 2025 11:28
Show Gist options
  • Save gterzian/9acd7ab1c783b198d0fec3bcb5fcdd09 to your computer and use it in GitHub Desktop.
Save gterzian/9acd7ab1c783b198d0fec3bcb5fcdd09 to your computer and use it in GitHub Desktop.

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...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment