ebiederm

89 karmajoined il y a 3 ans

Eric Biederman

comments

il y a 4 joursdiscuss

I think a better summary is that google gave someone the responsibility to ensure AI was developed and used ethically, and didn't give them the power to execute that responsibility.

Apparently google did not even give them the freedom to come to their own conclusions.

I just skimmed through the paper again and what it says seems to hold up well.

The paper is heritical in that it suggests slowing down, using carefully chosen less biased data, and understanding how it all works.

Basically challenging the AI bitter lesson.

I can see how that would meet with a lot of resistance from people who have gone all in on the bitter lesson.

il y a 9 joursdiscuss

What?

That post says very clearly at the beginning that hybrids are the preferred approach right now.

No one except the NSA actually wants a non-hybrid.

Which raises the question what is the NSA up to.

Especially since the NSA has a mission statement, a track record, and a billion dollar budget to subvert other peoples cryptography. When they aren't beyond transparent why should anyone give them the benefit of the doubt?

il y a 12 joursdiscuss

California has another distortion. The property value for tax purposes does not change unless you sell.

In many other states there is the lesser distortion of property valuearions for tax purposes not being allowed to go up faster than a roughly fized rate. Something like 3% a year.

At a practical level I wonder if limiting how much rents can increase from year to year would be a better policy, than not letting rent levels change at all.

Then there is the question of how to encourage home construction so there is sufficient supply where there is demand for people to live.

il y a 17 joursdiscuss

Dijkstra actually had a much more reasonable title on the article.

It was the editor of the publication Niklaus Wirth that changed the title to goto considered harmful.

Dijkstra was arguing for procedures with a single entry point and a single exit point. So it is easier to reason about what a procedure does.

il y a 17 joursdiscuss

Yeah no. Not really.

That is what was tried. The S&P 500 didn't play along.

A comparatively small number of index funds & retirement accounts that use them will get caught. The majority won't.

il y a 22 joursdiscuss

It is worth noting that register coalescing gets a lot of attention in interference graph coloring allocators because they typically have a pre-pass that inserts copies everywhere (because adding copies or spills later is so hard). So instead of worrying about where to insert copies and spills, those allocators worry about what to coalesce instead.

In my own compiler (where I don't add copies in a prepass) I have not yet found a case where any coalescing would be beneficial.

il y a 22 joursdiscuss

The big caveat in what I was saying is that it is only the pure graph coloring portion that has an optimal linear time algorithm.

Take code in static single assignment form, or another form where it is values that are tracked with live ranges. For a single basic block the interference graph of the live ranges is an interval graph. As the live ranges are just intervals from the instruction that produces the value to the last instruction that consumes the value.

It is annoying but totally doable to follow this into graph theory and see that interval graphs, are a subset of chordal graphs, and these graphs have an algorithm that colors the graph optimally in linear time.

Poke a little more and it turns out that algorithm is the same algorithm as linear-scan register allocation.

Add multiple basic blocks and it is trickier to see, but there are proofs in the academic literature that the interference graph remains an interval graph. Something about phi functions not counting.

Which is what I meant when I said a linear time algorithm.

Compare that to the O(N^2) heuristic from the paper register allocation by graph coloring.

The big change is going from a linear time optimal algorithm to a quadratic time heuristic and proclaiming the quadratic time heuristic is better. (What???)

In practice there are a lot of complications that are not accounted for by graph coloring. Instructions and function calls that take fixed registers. Spilling registers when you need more values alive then there are registers. Deliberately keeping a non-minimal number of values in registers to increase instruction level parallelism.

To the best of my knowledge all of those problems are very tractable if you start with a linear scan register allocator, as the code can be changed without requiring the register allocation to restart.

Code based on computing the interference graph has to reconpute the interference graph and restart whenever the code has to be changed. Making it much worse time wise. If for no other reason than computing the interference graph is O(N^2).

So yes more complications but only because the model described is overly simplified.

il y a 23 joursdiscuss

The academic literature on register allocation is scary.

First is presented a linear time optimal algorithm for graph coloring then it is claimed better can be done by a O(N^2) algorithm that uses a heuristic.

I do believe the dragon book got caught with the emperor's new register allocator and the literature hasn't really recovered yet.

il y a 24 joursdiscuss

Not who you asked but I took a quick look.

Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.

At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use.

I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.

il y a 24 joursdiscuss

Thank you. That makes things clearer.

I especially appreciate the trick of asserting the intermediate truth to help the prover along.

As someone who writes software I very much agree that verification of asserts before run time (written in the language itself) is very approachable to a programmer.

In a similar vein I agree with the folks at Jane Street that aiming to rule out specific classes of bugs (as opposed to proving a program is entirely correct) is a very practical goal.

il y a 26 joursdiscuss

> 36. The use of a program to prove the 4 color theorem will not change mathematics -- it merely demonstrates the theorem, a challenge for a century, is probably not important to mathematicians.

il y a 26 joursdiscuss

Have you looked at ADA Spark?

If you have does it match your intuition of how things should be done?

I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly.

So I would be interested in perspectives of people who have been down this route before.

le mois dernierdiscuss

It is talking about replacing a classic mark/sweep collector for unix domain sockets by something based on Tarjan's Strongly Connected Components.

le mois dernierdiscuss

Weird. The copy I read says they have just deleted that section of their user agreement.

le mois dernierdiscuss

Assuming this is correct that is a very intriguing result.

FP64 emulated with FP8 running faster than the native FP64 implementation.

le mois dernierdiscuss

How does it follow that there is no point in trying for formal correctness? In many problems there is an interesting subset that is quickly solvable even when the general case is not.

SAT solvers in practice are quick on just about everything.

SAT solvers being programs that solve the original NP-compete problem.

le mois dernierdiscuss

Please read the article.

The unsolicited security reports are the issue.

le mois dernierdiscuss

Thank you for posting this.

I had heard LLMs were finding a lot of bugs very quickly and now I can see what that looks like from a user perspective.

le mois dernierdiscuss

Hooray! A static test fire caught a problem.

Crap! There was a serious latent problem for the test fire to find.

il y a 2 moisdiscuss

Plus pretty blantant plagiarism.