> the most foundational distributed computing protocols—known as Paxos—meets its specifications.
> Paxos is one of the most important examples of the category
>“Most—if not all—consensus algorithms fundamentally derive concepts from Paxos,” Goel said.
A lot of burying the lede here, trying to imply Paxos powers many more applications than it actually does. While Paxos is in decent widespread use, and influential, I find some of the verbiage here lying by omission.
First, automatically checking Paxos is very cool. Nothing I'm saying in any way diminishes that achievement.
Next, the result is entirely unsurprising. Paxos is proved correct since its construction was formally derived[1] to be so.
Finally, this is a nice opportunity to highlight the distinction between program verification and program derivation. In general, it's considerably easier to derive a program that has a property than it is to verify that an arbitrary program has a property. For example the halting problem is uncomputable in general and yet it's easy for a competent programmer to derive loops that always terminate. This is analogous to how it's much easier to determine that some large number is the product of two primes when you yourself produced it by multiplying those same two primes than it is to factor the product when the multiplier and multiplicand are not already known.
That seems pretty accurate, TBH. Correct distributed consensus is almost exclusively done via some flavor of Paxos.
As for the actual research, it probably needs much closer reading, but if they can automatically infer nontrivial inductive invariants that's huge for automatic verification, since this is the usual stumbling block for those kinds of tools.
Most people have never dealt with large resilient systems, and do not understand what "distributed consensus" even means, and what it enables. Hence the derisive comments on this important result.
As I understand it, Raft is much more commonly relied upon than Paxos. Raft uses concepts from Paxos, but is not Paxos. So, a proof about Paxos is not a proof about Raft.
Raft is more or less a Paxos variant with good marketing. Sure, the proof for vanilla Paxos won't directly apply, but it's not inaccurate to say that it derives heavily from Paxos, which is all the quote above was saying. See https://emptysqua.re/blog/paxos-vs-raft/.
If you read the article, you can see that there are barely any material differences between Paxos and Raft. Certainly no more than there are between the description of a program as an abstract state machine and its actual implementation (and based on our other comment thread, you seem to be under the impression that there is not much difference there).
I don't need to read the article to know that Paxos and Raft have substantial commonality. That does not make them the same. That does not make a proof about one a proof about the other. That does not make a program that implements one a program that implements the other.
An abstract state machine, such as defines a version of Paxos, maps trivially one-to-one to parts of a program that implements it. A different abstract state machine, such as one that implements Raft, maps trivially one-to-one to a different program.
You might reasonably demonstrate that two different state machines define the same system behavior, but you would need to provide that demonstration. That has not been reported.
> The accelerators included within PS3’s Cell are the Synergistic Processor Element (SPE). Cell includes eight of them, although one is physically disabled during manufacturing.
This was disabled in software (by syscon) early on in the boot process. Many people "unlocked" theirs without stability issues. My understanding was that it was a yield thing, and definitely not intended for general use ;)
> This makes you wonder if IBM/Sony/Toshiba hit a wall while trying to scale Cell further, so Sony had no option but to get help from a graphics company.
Interviews from early 2nd party developers confirm this: https://www.ign.com/articles/2013/10/08/playstation-3-was-de...
That's also why the PS3 has two separate RAM, compared to the xbox 360's unified memory - Sony was trying to do that as well.
> HDMI connector
idk if anyone remembers this, but sony was talking about multi display gaming, such as having a status display. There was a prototype that had two hdmi ports and three ethernet - sony claimed it would also be a home server and router at that time. devkits did include two hdmi ports, and i suspect that the two screen claim was something that they made up almost on the spot, but who knows.
I'm trying to dig through this to understand what it means, but I am far from an expert on regulations or legalese. I'm looking forward to any breakdowns and explanations/annotations of the passages in this article and rule. If anyone has any, please let me know in the reply?
I'm a regulatory lawyer (but I have no experience with export controls) and I can't decipher the rule either. I actually wonder how anyone is able to confidently draft and revise such a long document with so many complex cross-references:
> License Exception ACE eligibility is added for 5E001.a (for 5A001.j, 5B001.a (for 5A001.j), 5D001.a (for 5A001.j), or 5D001.c (for 5A001.j or 5B001.a (for 5A001.j)). License Exception STA conditions is revised to remove eligibility for 5E001.a (for 5A001.j, 5B001.a (for 5A001.j), 5D001.a (for 5A001.j), or 5D001.c (for 5A001.j or 5B001.a (for 5A001.j)) to destinations listed in Country Groups A:5 and A:6 (See Supplement No. 1 to part 740 of the EAR for Country Groups). License Exception TSR is revised to remove eligibility for “technology” classified under ECCN 5E001.a for 5A001.j, 5B001.a (for 5A001.j), ECCN 5D001.a (for 5A001.j), or 5D001.c (for 5A001.j or 5B001.a (for 5A001.j)).
It's like a logic puzzle.
Edit: Looking at this random paragraph again and it seems they're missing a few closing parens so maybe the answer to how they confidently draft and revise these documents is... they don't.
I can’t help but wonder if encryption export controls will be slipped into this mess. Seems like a good place to hide them but I don’t have time to drudge through this at the moment.
I doubt it. The link says it’s consistent with Wassenaar Agreement (WA) negotiations, which is the international export control agreement that is quite well harmonized across many nations. WA has a lot of restrictions on encryption, but a huge carve out for most items that says encryption on commercially available devices is exempt.
Are you saying we're way past the point where encryption could be restricted from export in the U.S.? Because encryption exports are controlled and when I first started programming they were completely illegal. Every once in a while new legislation is proposed to make these exports illegal again, usually to "save the children".
Based on other comments here, I'll assume there is no hidden agenda on encryption here but a document this messy is probably hiding "stuff" (on purpose or not).
With AES widely available in free code, adding export controls today wouldn't seem to do much damage to symmetric crypto at least.
Maybe post-quantum schemes could be affected, but it's only a question of time until people agree on a standard, and if that one gets exported and doesn't get broken, controlling crypto exports won't prevent anyone from using secure ciphers.
Encryption is restricted from export in the US. I've had to submit forms to do things as trivial as buying microcontrollers from TI which happened to have AES instructions.
No idea why I can go into a store and buy an infinitely more powerful Intel laptop without a form, though.
- licensing: some people, myself included, think a FOSS/Libre license such as LGPL/GPL3 is better for people and society. Android is mostly apache, which means it's not resistant at all to a company "stealing" it without giving back to the community.
- dependency on google: like it or not, key components of android are completely maintained by google. That means that the future of an open platform is at the whims of one organization. Sure, you could fork, but android is a massive project and a small team could hardly keep up.
- "the core of android can still be used by any phone manufacturer": android, and the related IPs, is pretty firmly in the control of the US government. A lot of funding for non-android mobile OSes comes from other governments interested in a platform and support that is unencumbered from five eyes states
My personal opinion? Having more platforms is good, as are more compatibility layers. Android is more than just an OS or a platform, it's a set of ABIs for running apps that's used by over a billion people.
> Paxos is one of the most important examples of the category
>“Most—if not all—consensus algorithms fundamentally derive concepts from Paxos,” Goel said.
A lot of burying the lede here, trying to imply Paxos powers many more applications than it actually does. While Paxos is in decent widespread use, and influential, I find some of the verbiage here lying by omission.