MMU: The memory management unit, part of the CPU designed to allow an OS kernel to flexibly control how memory addresses used by a program map to physical RAM.

Page: A 4k region of memory addresses.

Anonymous: The page is just regular old memory used by a single process for general purposes, it's not part of e.g. a memory-mapped file.

Backing: The memory corresponding to a page. The kernel can direct the MMU to map any page to any part of RAM, or delete the mapping entirely.

Zero page: The kernel keeps a single 4 KB page filled with zeros (the "zero page").

Page fault: An error that occurs when you try to write a page that's not present, or write to a read-only page. Some page faults are normal and expected by the kernel, they support features like swapping, memory-mapped files, etc. Such "expected" page faults are invisible to your program. (On the other hand, an unexpected page fault occurs when your program just straight-up accesses an address it's not supposed to, which will end your program with a SIGSEGV signal -- an all-too-familiar experience for a C programmer.)

When you allocate say 4 MB of memory, the kernel simply sets it to 1k read-only copies of the 4 KB zero page. Then when your program tries to write to a page, it faults. The kernel handles this expected fault by assigning that page an individualized memory region. If a program allocates a lot of memory, it's only assigned memory for what it actually uses, when it first uses it. This is an optimization: Every program that allocates more memory than it needs is wasteful, but the kernel can recover that waste by not backing the allocation with memory -- the program has to prove each page is needed by writing to it.

Store to a freshly-faulted anonymous page: The program stored data to its own memory, which caused an expected page fault.

> becomes invisible to that same thread's reload ~10 instructions later

The thread fairly quickly tried to read the data from the same place in memory it had just written to. It doesn't get the same data back. This is a major problem that causes the program to malfunction and crash.

> A pagemap read at the instant of the fault shows the backing is the kernel's zero page

The expected fault occurred because the program tried to write to an address that was mapped to the zero page, probably because it's the first write to freshly allocated memory. (This rules out other reasons it might be faulted, e.g. the page had been swapped to disk.)

> concurrent munmap's TLB shootdown

The page table is big and slow so the CPU caches parts of it in an area called the TLB (translation lookaside buffer). munmap is a kernel function that removes the backing for an address region. Since munmap changes the mapping, it has to inform the MMU the relevant part of the TLB is no longer valid.

> per-VMA-lock anonymous-fault fast path

This is what the kernel does when the program first writes to a zero page. Saying it's the "fast path" implies there's some (slow) special case handling in the kernel code, but the bug doesn't trigger any of the special cases, we're in the most common case, which the kernel code tries to handle as quickly as possible because it has measurable impact on performance. I would guess per-VMA-lock has to do with how the kernel synchronizes this code (a "lock" is a basic synchronization primitive, you should be familiar with it if you do any kind of multithreaded programming).

> The mechanism localizes to the interaction between the per-VMA-lock anonymous-fault fast path and a concurrent munmap's TLB shootdown. A source-level review of Linux 7.0.12 identifies a specific race in that interaction

The mechanism: What's actually happening to cause the program not to be able to load data it just stored in memory.

Localizes: The cause of a problem like this is a needle in a haystack -- it could be caused by the program, the kernel or the hardware. The analysis has narrowed down the haystack to a specific part of the kernel code.

Race in that interaction: Two parts of the kernel code, (1) The kernel code for munmap and (2) the kernel code to handle a program's first write to the read-only zero page for a fresh allocation. These two parts work fine individually but the problem occurs when they both try to change the page tables / TLB at exactly the same time. This is quite a small, specific haystack compared to "somewhere in the program, kernel or hardware" we started with.

Take a corpus of problems you know the answers to, but the AI sometimes gets wrong [1]. Have the AI try to solve each problem and give you a 1-5 integer confidence score. The known proportion of correct answers in each bucket gives you a mapping from scores to probabilities [2].

[1] One possible corpus creation strategy might be math problems that you really need to run a program to solve. You can run the program to generate the correct answer key, but disallow tool calling for the AI.

[2] I'm pretty sure there's some stats wizardry that will let you put error bars on each bucket's probability based on the number of problems that end up in each bucket.

Comments URL: https://news.ycombinator.com/item?id=48769514

Points: 3

# Comments: 2

If "we need to store solar energy from summer to winter" is indeed a significant issue, maybe you could use the extra power in summertime to make natural gas [1] and then store the gas until you need it in the winter.

[1] https://www.terraformindustries.com/ is a startup working on turning solar power into natural gas

Anthropic addresses this head-on in the final section of the paper titled "What should we do?" If you convince the US government to slow AI development, you have to convince China too, otherwise you're not stopping self-improving AI at all, you're just throwing away the lead to China. If you convince China too, China or the US or both might go back on their word and build self-improving AI secretly, for greed of the benefits it could bring or fear the other will go back on their word.

What you really need is a non-proliferation regime like the one for nuclear weapons, where every country makes potentially dangerous AI illegal and lets foreign or international inspectors monitor to check that nobody's building illegal AI in secret. But monitoring seems hard; it's general-purpose computation. How do you check whether a given datacenter is training an illegal AI and not just serving websites, running detailed protein folding simulations, or mining crypto? For that matter, how do you know that a nondescript industrial facility hasn't been repurposed into a hidden datacenter for training illegal AI?

The real problem is that the price of electricity isn't high enough. When supply is running out, raise the price so supply and demand can find equilibrium, then invest the new revenue into increasing capacity.

I agree with other posters; Rabin deserves an HN black bar.

[1] Basically, the pumping lemma says if you feed a finite state machine a long enough input, the FSM must loop. You can delete the looping part of the input or insert extra copies of it; the FSM can't tell the difference, it has to give the same output. In theoretical computer science, the pumping lemma is usually introduced early, as the simplest example of a theorem that proves there are things that cannot be computed by a certain class of computing machines (FSMs).

I feel like this is one topic where using an LLM detracts from the author's thesis; doubly so if they don't disclose it.

Being able to transport it seems like an important piece of that puzzle.

Production and storage would need to be scaled by many orders of magnitude, but that's merely an engineering problem...right?

Since the dawn of the Internet era, we've had a legal principle that platforms are relatively shielded from liability for what their users do.

It's the Internet. There's sexual content and sketchy characters on it. Occasionally people will encounter them -- even if they're under 18.

Anyone who grew up in the mid-1990s or later, think back to your own Internet usage when you were under 18. You probably found something NSFW or NSFL, dealt with it, and came out basically OK after applying your common sense. Maybe it was shocking and mildly traumatizing -- but having negative experience is how we grow. Part of growing up is honing one's sense of "that link is staying blue" or "I'm not comfortable with this, it's time to GTFO". And it seems a lot safer if you encounter the sketchy side of humanity from the other side of a screen. Think about how a young person's exposure to the underbelly of humanity might have gone in pre-Internet times: Get invited to a party, find out it's in the bad part of town and there are a bunch of sketchy people there -- well, you're exposed to all kinds of physical risks. You can't leave the party as easily as you can put your phone down.

I stopped logging onto Facebook regularly around 2009; I only log in a couple times a year. I hate what Facebook has become in the past decade and a half.

But giving a site with millions of users a multi-hundred-million-dollar fine because some of those users behave badly seems...asinine.

If your kid is old enough and responsible enough to be given unsupervised Internet access, you'd better teach them how to deal with the skeevy stuff they might encounter.

You can get even more speedup by taking into account cache effects. When you cross out all the multiples of 3 you use 512MB of bandwidth. Then when you cross out all multiples of 5 you use 512MB more. Then 512MB again when you cross out all multiples of 7. The fundamental problem is that you have many partially generated cache-sized chunks and you cycle through them in order with each prime. I'm pretty sure it's faster if you instead fully generate each chunk and then never access it again. So e.g. if your cache is 128k you create a 128k chunk and cross out multiples of 3, 5, 7, etc. for that 128k chunk. Then you do the next 128k chunk again crossing out multiples of 3, 5, 7, etc. That way you only use ~512MB of memory bandwidth in total instead of 512MB per prime number. (Actually it's only really that high for small primes, it starts becoming less once your primes get bigger than the number of bits in a cache line.)

[1] https://en.wikipedia.org/wiki/Find_first_set

- Have you ever uploaded a container to Dockerhub or Quay.io?

- Does that container have an OS inside it that has user accounts?

- Before you answered parent post's questions, did it occur to you that you might have to update your Docker images to comply?

- Did you remember on your own that you also have to delete or update older Docker images to comply, or did you not think of that until you read this question?

After you've answered these questions, please re-answer the parent post's questions.

If you work on any programming project at all in any capacity:

- Are you confident your work doesn't fall afoul of this?

- Are you confident they won't decide to come after you anyway for insane political, bureaucratic or "seeing-like-a-state" dysfunctions?

- Are you willing to bet millions of dollars in potential fines that your answers to the previous two questions are correct?

- Keep the "Next" button greyed out until you add three forms of identification.

- Ask the user to take photos of their 3 forms of ID with a webcam. Ask the user to hold them in increasingly bizarre poses -- left hand, right hand, woven between your fingers, behind your ear, between your toes.

- Add an "accessibility" button. This button pops up a text box that advises you if you can't comply because you don't have hands, ears, feet or whatever (hey, some people don't and that's perfectly fine!) you can just use a picture of somebody else's body parts, and helpfully provides a menu of AI-generated pictures of human ears, hands, etc. for you to copy-paste.

- To preserve privacy, send the actual photos to /dev/null.

- The "verify the photo of my ID" button should check whether random.random() > 0.8. On average the user will require 5 tries per photo, or 15 tries total.

- Add a checkbox that says "I am not in the state of California". Upon clicking this checkbox the "Next" button becomes not grayed out and you can proceed without completing the identity checking process.

- If the user does not seem to have a webcam installed, all UI elements are grayed out except the "I am not in the state of California" checkbox.

- If the user is installing via command line, say "Are you in the state of California [y/n]?" If the answer does not start with 'N' or 'n', it will simply repeat the question.

- The list of acceptable identification shall be: Driver's license, learner's permit, Social Security card, library card, school identification, Boy / Girl Scout membership card, school yearbook photo, Burger King Kid's Club membership card, utility bill, ISP bill, Burger King receipt, Mahalo Rewards card, any receipt paid via credit card, birthday card, a photo of a printout of any email from OnlyFans, a photo of a DNS TXT record containing the string "CALIFORNIA", a photo of your X account with a blue check mark.

Verification gets sold as "bulletproof" but I'm skeptical for a couple reasons:

- How do you establish the relationship between the code and the theorem? Lean theorem can be applied to zlib implemented in Lean, what if you want to check zlib implemented in a normal programming language like C, JS, Zig, or whatever?

- How do you know the key properties mean what you think they mean? E.g. the theorem says "ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data" but it feels like it would be very easy to accidentally prove ∃ x s.t. decompress(compress(x)) == x while thinking you proved ∀ x, decompress(compress(x)) == x.

I've tried Lean and Coq and...I don't really like them. The proofs use specialized programming languages. And they seem deliberately designed to require you to use a context explorer to have any hope of understanding the proof at all. OTOH a normal unit test is written in a general purpose programming language (usually the same one as the program being tested), I'm much more comfortable checking that a Claude-written unit test does what I think it's doing than a Claude-written Lean proof of correctness.