petergeoghegan

> So this crash has done them no real harm and taught them all a valuable lesson. It’s something every generation goes through. Why can’t I be entertained by it also?

That also seems fine, provided you draw the distinction. (I don't claim to be any kind of arbiter of taste, but you asked, so I answered.)

Have you looked through the responses to the meltdown of Celsius on Twitter? In many individual cases these appear to be ordinary people, in shock at having lost practically everything. All I'm saying is that laughing at people like that seems to me to be in very poor taste.

Michael Saylor and his ilk are definitely fair game, though. Just be sure to leave some Schadenfreude for me!

> You can have schadenfreude at Bernie Madoff getting caught and still sympathize and/or empathize with his many, many victims.

Exactly. Madoff's crimes were despicable because of the way that they hurt individuals and families. The situation with crypto is potentially quite a lot worse than that was. And not just because of the overall scale.

Many individual retailer investors will never recover. This has the potential to do a great deal of damage to the fabric of society.

> I think the most horrible is when techies celebrate a crash, without thinking about the middle class/lower class people who may have lost their life savings

I absolutely loathe this article, but you have a point. It seems unseemly to engage in schadenfreude against gullible retail investors, many of which are legitimate victims. This point is not really related to the arguments put forth by the article itself, but it still seems like a point that should be made here.

> I also find the comparison to tech stocks odd. Stocks are, of course, a fever dream.

Very true. But arguments in favor of cryptocurrencies often rely on absurd false dichotomies that start from a reasonable premise, and take it somewhere wildly unreasonable. This is just one example.

My favorite example: the way that human beings believe that gold has intrinsic value is somewhat arbitrary and based on historical or cultural factors, so it might as well be completely arbitrary -- this distinction is meaningless and/or doesn't exist. (This ignores obvious factors, such as the fact that gold is used in various industrial contexts, despite its high cost. Just for starters.)

> Because many of the costs of their irresponsible practices are externalized.

I'm sure that that's true in at least some important cases. I don't see what it has to do with formal verification.

> And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. It changed software, but only a little bit.

There seems to have been something akin to an "accident chain", where a large number of things went wrong. Had any one of these things not happened, there might have been much less harm caused, or even no harm at all.

I will admit to being peevish about stuff like this. Some of the failures with Therac-25 were systems failures that had nothing to do with software per se (I'm not counting "software hubris" as a software problem). They were failures of process, problems with hardware interlocks, and even UI bugs that made the software confusing to operators.

I have nothing against formal methods, but they're no substitute for a deep and abiding paranoia.

> You can prove programs are correct. The only possible flaw they can have is the specification is wrong.

So specifications are kind of like programs?

Have you heard of logical positivism?

> That's very much not what I said. There may be many reasons.

My point was that it always seems to be some external factor. That strikes me as being very convenient.

> Assuming some conclusion without actual research is braindead.

I didn't think I assumed anything. Like anybody else, I have many things that I need to assess in my day to day life, and often deal with considerable uncertainty.

> One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.

"Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are domain specific, for all kinds of reasons.

Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time.

Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?

> Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs.

Serious question: do you really believe that?

> That's just stupid. Show me the studies.

There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.

How about: skeptical of formal verification?

This sounds like motivated reasoning to me. Have you heard of Therac-25?

You might be inclined to suggest that that could have been prevented if only they'd used formal methods. Perhaps that's true. It's something that could have been prevented in many different ways, though. Yet it still happened.

The most important job of VACUUM is usually to make sure that queries remain responsive -- it's roughly comparable to a "full scan" within generational garbage collectors (for managed language runtimes). VACUUM does reclaim space in various ways, but that's often considered to be of secondary importance.

In Postgres, the on-disk representation is virtually the same thing as the in-memory representation used by pages stored in the buffer cache. In a system like Aurora or Neon, the representation of pages in the buffer cache is identical to that of Postgres (or has very minimal divergence to deal with one or two isolated problems). That part doesn't really change, which makes it possible to have a very deep level of compatibility without much effort. So it's radically different in one narrow, scoped way, but otherwise very similar.

While the storage knows how to materialize pages on demand, these are not transactionally consistent pages -- they often need to be interpreted by using metadata about transaction commit status, just like in Postgres.

The difficulty comes from the fact that VACUUM requires most of the same state that is required when processing a user transaction. For example, VACUUM needs the commit log to check whether a given transaction ID is for a transaction that committed or aborted (VACUUM also truncates the commit log to remove information about older XIDs when it is no longer required).

Aurora Postgres does still have VACUUM, which seems to work in the same way -- which is the same in Neon. AWS have in the past promoted Aurora as having significantly better performance characteristics when VACUUM is run. That may well be true, but the benefits seem to come from not having to generate full page writes in WAL, which are a way of preventing a low-level problem called torn pages. Theoretically you could just turn off full-page writes in standard Postgres if you had hardware that offered atomic page writes, though I don't think that it's a widespread practice.

I spend most of my time working on problems with VACUUM in Postgres itself (I'm one of the committers). An approach to organizing storage within transactional constraints seems necessary to push vacuuming down to storage, and that would more than likely need plenty of work in Postgres itself to be practical -- since it would cross a few layers of abstraction. Currently heapam doesn't specifically try to keep tuples inserted around the same time together, so it's hard to make anything that VACUUM does work implicitly or logically.

Disclaimer: I work for Neon

There seems to be a perception among Rust programmers that C's status as a defacto standard came to be in spite of C's contradictions, rather than as a result of them. Skimming the Rustonomicon just now left me with the impression that at least one Rust person gets it. Though it still seemed as if the author felt the need to choose their words very carefully, lest they "make the memory model people angry".

It will be in Postgres 15, which will be out later in the year

> as of 2017 at least the plan was to implement merge using the underlying insert on conflict mechanism

That was something that was discussed at length at the time, but ultimately rejected. And so the implementation of MERGE in Postgres has essentially the same limitations as every other MERGE implementation that I'm familiar with.

Postgres clearly stresses the trade-off that MERGE makes in the docs, though. Which probably sets it apart.

> "every statement is atomic"

Statement-level atomicity doesn't mean that you cannot get race conditions like the one that I described - it just means that the statement succeeds or fails as a whole.

It's quite clear that you can get those race conditions in both Oracle and SQL Server's MERGE (same with the new Postgres implementation). Last I checked neither SQL Server nor Oracle address the fact that MERGE pretty much doesn't do what many of its users imagine it can do. (There is a narrow theoretical sense in which it does meet expectations provided serializable isolation level is used, but in practice that isn't worth much to users.)

> anyway my experience has been that adding the lock hints "fixes" the problem with pk violations during concurrent upserts and it seemed to be commonly known and widely used afaict

That's not my impression:

https://www.mssqltips.com/sqlservertip/3074/use-caution-with...

The Oracle docs introduce MERGE as follows:

"Use the MERGE statement to select rows from one or more sources for update or insertion into a table or view. You can specify conditions to determine whether to update or insert into the target table or view.

This statement is a convenient way to combine multiple operations. It lets you avoid multiple INSERT, UPDATE, and DELETE DML statements."

MERGE doesn't claim to work as an atomic statement, and doesn't work as an atomic statement in practice. In other words you can get a unique violation error where a "true upsert" would update the row instead. You can work around this "limitation" in MERGE by retrying the statement until it succeeds, but at that point you might as well use a regular INSERT instead.

The syntax for INSERT .. ON CONFLICT constrains the problem in certain ways, which is quite deliberate. It's a pretty faithful representation of what's really going on. Hiding that creates a lot of subtle but real problems.

Did you read the text that uhoh-itsmaciek posted?

> a proprietary syntax for upserting despite the common practice of using merge w/hints for doing upserts in most other engines

I was the primary author of the feature. That decision wasn't related to hints at all. MERGE just doesn't address the problem that I wanted to address.

I think that you must be referring to Oracle's ignore_row_on_dupkey_index. Is that really in widespread use? While it is technically a hint, it is unlike any other hint it at least one important way: it changes the semantics of the query!

The important point is that many (though not all) queries are executed by looking things up in indexes, as opposed to searching through all of the data in the table. The internal pages of a B-Tree index are typically a fraction of 1% of the total size of the index. And so you really only need to store a tiny fraction of all of the data in memory to be able to do no more than 1 I/O per point lookup, no matter what. Your table may grow, but the amount of pages that you need to go through to do a point lookup is essentially fixed.

This is a bit of a simplification, but probably less than you'd think. It's definitely true in spirit - the assumptions that I'm making are pretty reasonable. Lots of people don't quite get their head around all this at first, but it's easier to understand with experience. It doesn't help that most pictures of B-Tree indexes are very misleading. It's closer to a bush than to a tree, really.

Why would the database "allocate space" unless it was truly necessary, in any case? While char(n) works that way, most applications don't actually use it, no matter the underlying DB system.

> The bugs are not caused by speculative execution.

Actually, they are.

It seems like you're arguing against the existence of any kind of low-level hardware/software interface. C is strongly associated with that interface, but it isn't the same thing.

> I personally believe that we would be much better off with lower level instructions exposed to us, and putting the complexity in software

There have been several initiatives that sound vaguely like that, none of which actually worked out commercially. Principally Itanium. At the same time, there is no question that it's possible to gain a lot in performance if you're both willing and able to use a programming environment like CUDA.

It seems to me that the article never actually articulates an alternative in enough detail to take seriously. It doesn't seem to make any falsifiable claim.

In my view the most plausible explanation for why things in this area look the way they look was articulated in DJB's "The Death of Optimizing Compilers" talk. I'm not surprised that this ACM piece was written by somebody that works on optimizing compilers. Perhaps that shouldn't be relevant, but I can't help but suspect that it is.

CONCURRENTLY needs to wait for old transactions to go away, including those that haven't (and won't ever) touch the table that you're building an index on. So it's not waiting for a lock as such - it's waiting for older transactions to go away without conflicting in a way that can cause these "traffic jams". This can be a problem for the obvious reason, though generally only for the index build itself.

Tricky problems with relation-level locks tend to come from a combination of one lock request that is "generally non-disruptive but long-lived", and another lock request that is "generally disruptive/blocking but short-lived". I have heard of quite a few problem scenarios where these locks conflict with each other (usually by chance), leading to "generally disruptive/blocking and long-lived" -- which can be very dangerous. But that's fundamental to how lock managers work in general.

The Postgres implementation tries to make it as unlikely as reasonably possible. For example, autovacuum usually notices when something like this happens, and cancels itself.

> In Postgres, by contrast, any schema change, even adding an index with the CONCURRENTLY option, needs to at least momentarily hold a totally exclusive lock that blocks all writes and reads on the table.

It's true that every DDL statement requires a relation-level lock. Though the same is true for even a simple SELECT statement. The important detail is the lock strength for each variety of DDL, and how that affects and interacts with other queries (including other DDL):

https://www.postgresql.org/docs/devel/explicit-locking.html#...

CREATE INDEX (even without CONCURRENTLY) will not block reads, even for a moment (it just blocks write DML). CREATE INDEX (without CONCURRENTLY) won't even block other CREATE INDEX statements that run against the same table.

My guess is that your application appeared to exhibit this behavior, but the true problem was actually how several conflicting locks accumulated, which had the effect of blocking SELECTs for an unreasonably long time. A combination of CREATE INDEX and some other conflicting DDL that really does block reads (e.g., certain kinds of ALTER TABLE) can create the false impression that CREATE INDEX blocks reads in general. But that's not really the case at all. At worst, CREATE INDEX is only one part of the "traffic jam" that caused SELECTs to block in this scenario.

> That these two entities overlap so much is a very bad thing, and definitely a liability if things turn bad from a legal perspective.

You are the one that is filing confusing, duplicative trademark and servicemark claims that waste the community's time. You seem to be asking me to put that aside for a moment. But I'm not willing to do that for reasons that will be obvious to most people.

> The PostgreSQL Association of Canada; Postgres Europe; and Fundación PostgreSQL will transfer...

The first two organizations are almost the same thing as the core team, for all practical purposes (unless you're a lawyer, say). There is very significant overlap in membership. A cosy arrangement, certainly. I imagine that this structure was based on certain practical considerations. Legal advice about IP and whatnot.

I have been working on Postgres (primarily as a Postgres backend hacker) for over a decade now. The people from the first two groups are friends and colleagues. There are problems, but on the whole these people have a significant amount of moral authority for good reasons. They have at least gotten us this far.

The idea that one of the first two organizations from your list are at risk of going rogue is beyond ludicrous. There are certainly legitimate criticisms that one could make about the project's governance, but this isn't one of them.

> It's just that we disagree what the governing bodies of that community should be, believing that the current ones are a great liability and need urgent reform.

This is not reform. This is a clumsily executed power grab.

> No, the Founder's are the Founding members (5).

The document says:

"The Founder [singular], Mr. Alvaro Carlos Hernandez Tortosa, is Honorary Life Member..."

It goes on to say:

"...the willingness of the Founder [singular] expressed in this Statutes"

See why I'm connecting the two sentences?

Don't you think that this choice of words is, at the very least, confusing? Maybe you should issue a clarification on your blog. Perhaps it's all just a misunderstanding.

> This is what is called "the founder's will".

Just to be clear: you're saying that "the founder's will" should not be interpreted as meaning "what Alvaro Carlos Hernandez Tortosa [the founder for life] decides"?