Add a comment on HW queue

theories/examples/queue/proof_hw_graph.v

@@ -2827,6 +2827,10 @@ Proof.
 Qed.
 End proof.
 
+(** Both weak and strong HW queue implementations satisfy our weak spec, which
+  is stronger than Yacovet's weak spec.
+  However, unlike Yacovet, we don't have a proof that the strong HW queue has a
+  linearization. *)
 Definition hwqueue_impl (sz : positive) (b : bool)
   Σ `{!noprolG Σ, !hwqG Σ, !atomicG Σ} :
   weak_queue_spec Σ := {|