The Codex agent is only given tools to edit the single HTML file that displays on the homepage. The page is on a separate domain, so there's no cookie sharing, and the iFrame is in a sandbox. That said, the biggest risk is social engineering attacks.
Hi all - this is a small research prototype I built to explore cross-GPU reuse of transformer attention states.
When inference engines like vLLM implement prefix/KV caching, it's local to each replica. LMCache recently generalized this idea to multi-tier storage.
KV Marketplace focuses narrowly on the GPU-to-GPU fast path: peer-to-peer prefix reuse over RDMA or NVLink. Each process exports completed prefix KV tensors (key/value attention states) into a registry keyed by a hash of the input tokens and model version. Other processes with the same prefix can import those tensors directly from a peer GPU, bypassing host memory and avoiding redundant prefill compute.
Under optimistic conditions (perfect prefix importing), the prototype shows about a 15% reduction in latency and throughput gains without heavy tuning. The code is intentionally minimal (no distributed registry, eviction, or CPU/disk tiers yet) but it's a prototype of "memcached for attention."
I thought others exploring distributed LLM inference, caching, or RDMA transports might find the repo useful or interesting.
Oh really? I can't find anything about the memory model online. I'm not sure what's the best way to do this, but if there's a way for us to get in contact, I'd be interested in adjusting the project so it's developed in the most ergonomic way possible. I'm chatting with a couple of universities and I might issue a research grant for this project to be further fleshed out, so would be keen to hear your insights prior to kicking this off. My email is neel[at]berkeley.edu.
Hi all, this is a small research prototype I built that connects Rust's MIR (Mid-level IR) to Coq, the proof assistant used for formal verification.
cuq takes the MIR dump of a Rust CUDA kernel and translates it into a minimal Coq semantics that emits memory events, which are then lined up with the PTX memory model formalized by Lustig et al., ASPLOS 2019.
Right now it supports:
* a simple saxpy kernel (no atomics)
* an atomic flag kernel using acquire/release semantics
* a "negative" kernel that fails type/order checking
The goal isn't a full verified compiler yet. It's a first step toward formally checking the safety of GPU kernels written in Rust (e.g. correct use of atomics, barriers, and memory scopes).
Happy to hear thoughts from folks working in Rust verification, GPU compilers, or Coq tooling.