David Dill
@davidldill.bsky.social
Donald E. Knuth Professor, Emeritus, in the School of Engineering, Stanford University.
Working on formal verification, dipping my toes into AI.
Founder of VerifiedVoting.org, which advocates reforms to make elections more trustworthy.
Working on formal verification, dipping my toes into AI.
Founder of VerifiedVoting.org, which advocates reforms to make elections more trustworthy.
Find a few specific examples of grants that are most understandable to the public an obviously beneficiary (e.g., breakthrough cancer or other disease treatments) and ask what the process was that led to cutting them.
Or other specific cuts that are indefensible.
Or other specific cuts that are indefensible.
June 11, 2025 at 4:13 PM
Find a few specific examples of grants that are most understandable to the public an obviously beneficiary (e.g., breakthrough cancer or other disease treatments) and ask what the process was that led to cutting them.
Or other specific cuts that are indefensible.
Or other specific cuts that are indefensible.
This is an excellent opportunity for Elon to learn about "empathy".
June 5, 2025 at 8:52 PM
This is an excellent opportunity for Elon to learn about "empathy".
And this is enforcing demands that were in a letter the administration sent BY MISTAKE!
May 6, 2025 at 12:24 AM
And this is enforcing demands that were in a letter the administration sent BY MISTAKE!
I was an NSF investigator for many years. I posted results of one of my research projects, just as one example of many thousands of NSF projects that have led to U.S. dominance in science and tech.
Almost no one knows about these projects, but they're still important.
bsky.app/profile/davi...
Almost no one knows about these projects, but they're still important.
bsky.app/profile/davi...
Since the National Science Foundation is under threat, I thought I'd share one example of how NSF funding has benefited the U.S. (long)
It's not the most important example. Maybe it's an average innovation out of thousands funded by the NSF.
It's not the most important example. Maybe it's an average innovation out of thousands funded by the NSF.
May 2, 2025 at 11:32 PM
I was an NSF investigator for many years. I posted results of one of my research projects, just as one example of many thousands of NSF projects that have led to U.S. dominance in science and tech.
Almost no one knows about these projects, but they're still important.
bsky.app/profile/davi...
Almost no one knows about these projects, but they're still important.
bsky.app/profile/davi...
I don't know Jay Bhattacharya personally, but it's hard to believe that he wrote the quoted paragraph, which appears to be totally ignorant about what NIH actually does. It seems to consist of a bunch of talking points from right-wing media talking heads.
I'll let others debunk the misinformation.
I'll let others debunk the misinformation.
May 2, 2025 at 3:57 PM
I don't know Jay Bhattacharya personally, but it's hard to believe that he wrote the quoted paragraph, which appears to be totally ignorant about what NIH actually does. It seems to consist of a bunch of talking points from right-wing media talking heads.
I'll let others debunk the misinformation.
I'll let others debunk the misinformation.
The return on investment is hard to estimate, but it's obviously huge.
So, why am I reading articles about devastating cuts in NSF funding? Has anyone thought about this at all?
So, why am I reading articles about devastating cuts in NSF funding? Has anyone thought about this at all?
May 1, 2025 at 8:58 PM
The return on investment is hard to estimate, but it's obviously huge.
So, why am I reading articles about devastating cuts in NSF funding? Has anyone thought about this at all?
So, why am I reading articles about devastating cuts in NSF funding? Has anyone thought about this at all?
Again, NSF is responsible for thousands and thousands of innovations that have made the modern world. Murphi made an important difference, but it's a tiny fraction of the work funded by NSF.
For this reason, NSF has been enthusiastically supported by Democrats and Republican alike.
For this reason, NSF has been enthusiastically supported by Democrats and Republican alike.
May 1, 2025 at 8:58 PM
Again, NSF is responsible for thousands and thousands of innovations that have made the modern world. Murphi made an important difference, but it's a tiny fraction of the work funded by NSF.
For this reason, NSF has been enthusiastically supported by Democrats and Republican alike.
For this reason, NSF has been enthusiastically supported by Democrats and Republican alike.
Computers are (fairly) reliable because of many tools like Murphi that you probably haven't heard about.
Murphi was funded by additional sources besides the NSF, but I wouldn't have been able to start the project without NSF.
Murphi was funded by additional sources besides the NSF, but I wouldn't have been able to start the project without NSF.
May 1, 2025 at 8:58 PM
Computers are (fairly) reliable because of many tools like Murphi that you probably haven't heard about.
Murphi was funded by additional sources besides the NSF, but I wouldn't have been able to start the project without NSF.
Murphi was funded by additional sources besides the NSF, but I wouldn't have been able to start the project without NSF.
I think the first Murphi paper was published in 1991.
Recently, I was contacted by another former student that Murphi was being used at a very important computer company <redacted>, and that it was still regarded as the best tool in industry for debugging cache coherence protocols.
Recently, I was contacted by another former student that Murphi was being used at a very important computer company <redacted>, and that it was still regarded as the best tool in industry for debugging cache coherence protocols.
May 1, 2025 at 8:58 PM
I think the first Murphi paper was published in 1991.
Recently, I was contacted by another former student that Murphi was being used at a very important computer company <redacted>, and that it was still regarded as the best tool in industry for debugging cache coherence protocols.
Recently, I was contacted by another former student that Murphi was being used at a very important computer company <redacted>, and that it was still regarded as the best tool in industry for debugging cache coherence protocols.
One of my PhD students (trained with this and other funding) went to Intel to debug cache coherence protocols in their processors.
A LONG time ago, I ran out of students to maintain Murphi. The Murphi source code was distributed by other researchers at other schools, who had improved it.
A LONG time ago, I ran out of students to maintain Murphi. The Murphi source code was distributed by other researchers at other schools, who had improved it.
May 1, 2025 at 8:58 PM
One of my PhD students (trained with this and other funding) went to Intel to debug cache coherence protocols in their processors.
A LONG time ago, I ran out of students to maintain Murphi. The Murphi source code was distributed by other researchers at other schools, who had improved it.
A LONG time ago, I ran out of students to maintain Murphi. The Murphi source code was distributed by other researchers at other schools, who had improved it.
In the early years, I'd hear from people that it was being used routinely at their company and there were local experts who used it full time to debug their protocols.
At some point, it dawned on me that many major computer manufacturers were using Murphi as a design tool.
At some point, it dawned on me that many major computer manufacturers were using Murphi as a design tool.
May 1, 2025 at 8:58 PM
In the early years, I'd hear from people that it was being used routinely at their company and there were local experts who used it full time to debug their protocols.
At some point, it dawned on me that many major computer manufacturers were using Murphi as a design tool.
At some point, it dawned on me that many major computer manufacturers were using Murphi as a design tool.
Cache coherence protocols are *really* hard to get right, so we found weird bugs all over the place.
We made the program free and open source to minimize barriers to use in industry.
Pretty soon, people at major computer companies started using it.
We made the program free and open source to minimize barriers to use in industry.
Pretty soon, people at major computer companies started using it.
May 1, 2025 at 8:58 PM
Cache coherence protocols are *really* hard to get right, so we found weird bugs all over the place.
We made the program free and open source to minimize barriers to use in industry.
Pretty soon, people at major computer companies started using it.
We made the program free and open source to minimize barriers to use in industry.
Pretty soon, people at major computer companies started using it.
With some of my NSF funding, I started a few students working on this problem. We developed a program called "Murphi" for checking cache coherence protocols.
We tried it out on protocols being developed in our building, and a few in local industry (in Silicon Valley).
We tried it out on protocols being developed in our building, and a few in local industry (in Silicon Valley).
May 1, 2025 at 8:58 PM
With some of my NSF funding, I started a few students working on this problem. We developed a program called "Murphi" for checking cache coherence protocols.
We tried it out on protocols being developed in our building, and a few in local industry (in Silicon Valley).
We tried it out on protocols being developed in our building, and a few in local industry (in Silicon Valley).
The problem with caches of a shared memory is that it's complicated to maintain consistency. There are various protocols (collections of rules) to do this.
I just deleted an explanation because it gets too involved, so I'll ask you to trust me on this.
I just deleted an explanation because it gets too involved, so I'll ask you to trust me on this.
May 1, 2025 at 8:58 PM
The problem with caches of a shared memory is that it's complicated to maintain consistency. There are various protocols (collections of rules) to do this.
I just deleted an explanation because it gets too involved, so I'll ask you to trust me on this.
I just deleted an explanation because it gets too involved, so I'll ask you to trust me on this.
To make it the memory appear faster, computers use "caches" -- small, close memories that keep a copies of frequently-used memory locations for fast access. The circuitry moves data in and out of the cache as necessary.
May 1, 2025 at 8:58 PM
To make it the memory appear faster, computers use "caches" -- small, close memories that keep a copies of frequently-used memory locations for fast access. The circuitry moves data in and out of the cache as necessary.
So cell phones and laptops are shared memory multiprocessors.
I went to neighboring offices asking: What are your biggest worries about bugs? They said "cache coherence".
Here's the problem: In electrical terms, a shared memory is big and far away and thus slow.
I went to neighboring offices asking: What are your biggest worries about bugs? They said "cache coherence".
Here's the problem: In electrical terms, a shared memory is big and far away and thus slow.
May 1, 2025 at 8:58 PM
So cell phones and laptops are shared memory multiprocessors.
I went to neighboring offices asking: What are your biggest worries about bugs? They said "cache coherence".
Here's the problem: In electrical terms, a shared memory is big and far away and thus slow.
I went to neighboring offices asking: What are your biggest worries about bugs? They said "cache coherence".
Here's the problem: In electrical terms, a shared memory is big and far away and thus slow.
So, I was in a building with researchers designing "shared memory multi-processors". These are machines with multiple CPUs that interact by sharing memory. Back then, each CPU was a separate chip, and these were big machines.
Nowadays, all multi-core CPUs are shared memory multiprocessors.
Nowadays, all multi-core CPUs are shared memory multiprocessors.
May 1, 2025 at 8:58 PM
So, I was in a building with researchers designing "shared memory multi-processors". These are machines with multiple CPUs that interact by sharing memory. Back then, each CPU was a separate chip, and these were big machines.
Nowadays, all multi-core CPUs are shared memory multiprocessors.
Nowadays, all multi-core CPUs are shared memory multiprocessors.
My research area was a new approach to checking the correctness of digital circuits, called "model checking". The theory had been developed by my advisor and his students a few years before, and a lot of my graduate research was in finding practical applications.
May 1, 2025 at 8:58 PM
My research area was a new approach to checking the correctness of digital circuits, called "model checking". The theory had been developed by my advisor and his students a few years before, and a lot of my graduate research was in finding practical applications.
At the time, it was enough to fund a couple of PhD students, some travel, maybe summer salary (professors often get paid for 9 out of 12 months. At major research institutions, they don't take the summer off. They spend it focusing on research, and get paid from research grants.)
May 1, 2025 at 8:58 PM
At the time, it was enough to fund a couple of PhD students, some travel, maybe summer salary (professors often get paid for 9 out of 12 months. At major research institutions, they don't take the summer off. They spend it focusing on research, and get paid from research grants.)
Before I took the position, I had written a short application for an NSF "Presidential Young Investigator" award. At that time, it was a startup grant for the first 5 years of a small number of junior researchers.
I found out in my first year that I got one of these.
I found out in my first year that I got one of these.
May 1, 2025 at 8:58 PM
Before I took the position, I had written a short application for an NSF "Presidential Young Investigator" award. At that time, it was a startup grant for the first 5 years of a small number of junior researchers.
I found out in my first year that I got one of these.
I found out in my first year that I got one of these.
But sometimes a story about one thing helps people understand better than a bunch of statistics.
I finished my PhD in computer science and was lucky enough to get an Assistant Professor position at Stanford, which has a *really* good CS department.
I finished my PhD in computer science and was lucky enough to get an Assistant Professor position at Stanford, which has a *really* good CS department.
May 1, 2025 at 8:58 PM
But sometimes a story about one thing helps people understand better than a bunch of statistics.
I finished my PhD in computer science and was lucky enough to get an Assistant Professor position at Stanford, which has a *really* good CS department.
I finished my PhD in computer science and was lucky enough to get an Assistant Professor position at Stanford, which has a *really* good CS department.
At best, it will be a slow, costly process of digging ourselves out of a deep hole.
At worst, we're bringing on the new Dark Ages.
At worst, we're bringing on the new Dark Ages.
March 23, 2025 at 10:14 PM
At best, it will be a slow, costly process of digging ourselves out of a deep hole.
At worst, we're bringing on the new Dark Ages.
At worst, we're bringing on the new Dark Ages.
If the university agrees, they can be partially reactivated to supervise grants, etc.
So, what this is about, is Stanford allowing Bhattacharya to retire, and not violating its own rules about his post-retirement status.
So, what this is about, is Stanford allowing Bhattacharya to retire, and not violating its own rules about his post-retirement status.
March 23, 2025 at 4:41 PM
If the university agrees, they can be partially reactivated to supervise grants, etc.
So, what this is about, is Stanford allowing Bhattacharya to retire, and not violating its own rules about his post-retirement status.
So, what this is about, is Stanford allowing Bhattacharya to retire, and not violating its own rules about his post-retirement status.