There's precedent for this. In many biology experiments, the "raw data" is an actual organism, like a colony of bacteria or something. There are scientific protocols for accessing that "data", but you have to be able to prove that you are an institution that can handle it. Even if the public "owns" it, technically speaking, no reputable scientist is going to send an e. coli sample to just anyone.
So I think we all understand that, in practice, we mean different things by "public access". Sometimes that means that anyone should be able to download the data, and sometimes that means that anyone should be allowed to go there and examine it for themselves.
You know who needs to introduce this rule? The ACM.
I'm fed up with so-called scientific papers with results based on proprietary software. It doesn't even have to be open source, though that would clearly be good for peer review. If I can't (given appropriate hardware and other appropriate caveats) run your software, I can't replicate your results. If I can't replicate your results, it's not science.
Not exactly. Machine-checkable outputs tend to come in one of two varieties: certificates (of which this is an example, since it's an UNSAT certificate) and proofs proper.
Proofs (which are the sort of things you'd feed to Coq or Isabelle) tend to rely heavily on built-in tactics. There are some theories (classical logic, intuitionistic logic, Presburger arithmetic, Tarski arithmetic, etc) which are known to be decidable, but the decision procedures are beyond most humans, let alone trained monkeys. For example, in Tarski arithmetic, you might be faced with the following goal:
a : R, b : R, c : R |- exists x : R, a*x*x + b*x + c = 0
(Translation into high-school-level maths: If a, b, and c are real numbers, then the equation ax^2 + bx + c = 0 has a real root.)
You apply the "eliminate the existential quantifier" tactic, and it will give you a new goal which represents the necessary and sufficient conditions for this goal to be true:
a : R, b : R, c : R |- (a = 0/\ b = 0/\ c = 0) \/ (a = 0/\ b 0) \/ (b*b >= 4*a*c)
(Translation into high-school-level maths: Either a, b and c are all zero, or the equation is really linear and nondegenerate, or the determinant is greater than or equal to zero. Yes, this result was really found automatically by a Tarski arithmetic solver.)
That's one "step" in a machine-checked proof. Most humans are not able to get the nondegeneracy conditions correct, and asking a trained monkey to do it is unreasonable.
The other type of check is a certificate. Certificates are technically proofs, but they are are typically highly domain-specific descriptions based the problem at hand, as opposed to a general statement in logic-plus-theories. Certificates for UNSAT, for example, tend to be based around a set of choices that a SAT solver would have to make to verify that the problem fails SAT.
Coq and Isabelle are far better choices, being better supported and open source. And if you need their credentials, there is a Coq-checked proof of the four colour theorem, and an Isabelle proof that the L4 kernel is secure.
I wrote my fair share of MODs back in the day; I'm familiar with all the tricks. Writing MODs was a different kind of fun than modern systems, but it was still fun.
The question was which one you like better. My personal opinion is that not being forced into technical limitations is easier, but it doesn't necessarily make you more creative to have more options.
The Beatles (a.k.a. the white album) was recorded on 4 tracks. The Dark Side of the Moon and Tubular Bells were recorded on 16 tracks. Pro Tools gives you a few hundred tracks, and it's fair to say that modern musicians don't do proportionally more with what they have. You get pretty much the same "amount" of music/production (less, sometimes; as Arnold Schoenberg famously pointed out, a rest is never a wrong note), but you get it faster and cheaper.
Breaking Bad season 5 has not yet screened on the ABC. If you wanted to watch it while the global conversation about it was still happening, you needed Foxtel with a Showcase subscription, which will set you back $72 a month. (For comparison, the DVD box set for season 5 costs less than half that, and you get to keep it.)
There was no other way to legally watch it in Australia. Most people can't justify spending $72 a month for one or two TV shows (say, Breaking Bad and Game of Thrones), and companies like AMC and HBO provide no other way, such as a streaming web site. It's unsurprising that Australia leads the world in pirating shows like these when the distributors refuse to take Australia's money. It's like The Oatmeal's experience only worse.
Note to AMC and HBO: No, I haven't pirated your damn shows. I've only seen a couple of episodes of Breaking Bad on free-to-air, and I have not seen any of Game of Thrones. I'd rather be out of the conversation completely than give any legitimacy to your price-gouging deals with Foxtel. There are people with money who would like to give it to you in return for content that you produce. It is your stupidity and ineptitude which is preventing said people from giving you said money. Fix that, and the piracy rate will drop dramatically.
I agree that the severity of the case is irrelevant. The number that I want to know is: In how many of those 8162 cases had charges not been filed?
Obviously different countries have different legal systems, but where I live, requesting an extradition without first charging someone with any crime at all is very unusual indeed.
No, you aren't. This was a key point in Liedtke's design for L4.
A "context switch" in a macrokernel OS (on Intel hardware; architectures which support tagged TLBs have a different tradeoff) is a single thing. In L4, the various parts of a context switch are decoupled and the kernel tries very hard to only do as much as it needs to. For commonly-accessed drivers, for example, an IPC round-trip requires only a selector switch (which a macrokernel OS does anyway when it enters and exits kernel mode) and avoids the address space switch completely.
Of course, none of this applies to Mach, which isn't a "micro"-kernel by modern standards.
On the P4, the expensive part was entering and exiting kernel mode; it even dominated address space switching and TLB reload for typical scenarios. I don't know about modern CPUs, but the key point remains: "extra context switching [...] kills performance" is a claim that's hard to prove.
High frequency trading systems are not a typical example of anything, and should be held as a typical use case for any reasonable operating system. They do things like use custom network hardware which plays fast and loose with the standards, and could easily be compromised if they weren't on a fairly trusted network.
Slashdot Mirror
Yeah, we're not talking about Lemelson here.
The idea is not mine; I'm actually paraphrasing Richard Lenski.
Wrong show. What we need is the Prototypers to build something to clean up the site.
(Unless it was them who actually contaminated the site in the first place.)
The "useful idiot" pay grade is surprisingly low. Which reminds me, I didn't get my check this month.
Oh, that's easy: It's because he's a nerd. He's one of us.
We don't discriminate. We do the same to Linus, RMS, and ESR.
There's precedent for this. In many biology experiments, the "raw data" is an actual organism, like a colony of bacteria or something. There are scientific protocols for accessing that "data", but you have to be able to prove that you are an institution that can handle it. Even if the public "owns" it, technically speaking, no reputable scientist is going to send an e. coli sample to just anyone.
So I think we all understand that, in practice, we mean different things by "public access". Sometimes that means that anyone should be able to download the data, and sometimes that means that anyone should be allowed to go there and examine it for themselves.
You know who needs to introduce this rule? The ACM.
I'm fed up with so-called scientific papers with results based on proprietary software. It doesn't even have to be open source, though that would clearly be good for peer review. If I can't (given appropriate hardware and other appropriate caveats) run your software, I can't replicate your results. If I can't replicate your results, it's not science.
We always get the heroes we're given, not the ones we want.
Not exactly. Machine-checkable outputs tend to come in one of two varieties: certificates (of which this is an example, since it's an UNSAT certificate) and proofs proper.
Proofs (which are the sort of things you'd feed to Coq or Isabelle) tend to rely heavily on built-in tactics. There are some theories (classical logic, intuitionistic logic, Presburger arithmetic, Tarski arithmetic, etc) which are known to be decidable, but the decision procedures are beyond most humans, let alone trained monkeys. For example, in Tarski arithmetic, you might be faced with the following goal:
a : R, b : R, c : R |- exists x : R, a*x*x + b*x + c = 0
(Translation into high-school-level maths: If a, b, and c are real numbers, then the equation ax^2 + bx + c = 0 has a real root.)
You apply the "eliminate the existential quantifier" tactic, and it will give you a new goal which represents the necessary and sufficient conditions for this goal to be true:
a : R, b : R, c : R |- (a = 0 /\ b = 0 /\ c = 0) \/ (a = 0 /\ b 0) \/ (b*b >= 4*a*c)
(Translation into high-school-level maths: Either a, b and c are all zero, or the equation is really linear and nondegenerate, or the determinant is greater than or equal to zero. Yes, this result was really found automatically by a Tarski arithmetic solver.)
That's one "step" in a machine-checked proof. Most humans are not able to get the nondegeneracy conditions correct, and asking a trained monkey to do it is unreasonable.
The other type of check is a certificate. Certificates are technically proofs, but they are are typically highly domain-specific descriptions based the problem at hand, as opposed to a general statement in logic-plus-theories. Certificates for UNSAT, for example, tend to be based around a set of choices that a SAT solver would have to make to verify that the problem fails SAT.
Coq and Isabelle are far better choices, being better supported and open source. And if you need their credentials, there is a Coq-checked proof of the four colour theorem, and an Isabelle proof that the L4 kernel is secure.
I may have misread my source. DSOTM was mixed with a single 16-track mixer, but I'm certain there was a lot of two-generation mastering going on.
I wrote my fair share of MODs back in the day; I'm familiar with all the tricks. Writing MODs was a different kind of fun than modern systems, but it was still fun.
The question was which one you like better. My personal opinion is that not being forced into technical limitations is easier, but it doesn't necessarily make you more creative to have more options.
I suspect this isn't just true of games.
The Beatles (a.k.a. the white album) was recorded on 4 tracks. The Dark Side of the Moon and Tubular Bells were recorded on 16 tracks. Pro Tools gives you a few hundred tracks, and it's fair to say that modern musicians don't do proportionally more with what they have. You get pretty much the same "amount" of music/production (less, sometimes; as Arnold Schoenberg famously pointed out, a rest is never a wrong note), but you get it faster and cheaper.
Breaking Bad season 5 has not yet screened on the ABC. If you wanted to watch it while the global conversation about it was still happening, you needed Foxtel with a Showcase subscription, which will set you back $72 a month. (For comparison, the DVD box set for season 5 costs less than half that, and you get to keep it.)
There was no other way to legally watch it in Australia. Most people can't justify spending $72 a month for one or two TV shows (say, Breaking Bad and Game of Thrones), and companies like AMC and HBO provide no other way, such as a streaming web site. It's unsurprising that Australia leads the world in pirating shows like these when the distributors refuse to take Australia's money. It's like The Oatmeal's experience only worse.
Note to AMC and HBO: No, I haven't pirated your damn shows. I've only seen a couple of episodes of Breaking Bad on free-to-air, and I have not seen any of Game of Thrones. I'd rather be out of the conversation completely than give any legitimacy to your price-gouging deals with Foxtel. There are people with money who would like to give it to you in return for content that you produce. It is your stupidity and ineptitude which is preventing said people from giving you said money. Fix that, and the piracy rate will drop dramatically.
We have QuickFlix, but it's not the same.
I don't know about that. My experience is they're still good after 7 years and don't need any follow-up jokes.
That wasn't my claim.
What a great story that is. How often does it actually happen in practice, as a percentage of actual sexual assaults?
I agree that the severity of the case is irrelevant. The number that I want to know is: In how many of those 8162 cases had charges not been filed?
Obviously different countries have different legal systems, but where I live, requesting an extradition without first charging someone with any crime at all is very unusual indeed.
I find it cute that you think a thousand people all yelling "FUCK BETA" at the same time constitutes "deep intellectual stimulation".
What's wrong with plain old STL? It's not compatible with the current revision of the C++ standard library.
(You do know that the STL is the name for a specific library that predates ISO C++, right?)
They did play with L4, which is an even better choice.
No, you aren't. This was a key point in Liedtke's design for L4.
A "context switch" in a macrokernel OS (on Intel hardware; architectures which support tagged TLBs have a different tradeoff) is a single thing. In L4, the various parts of a context switch are decoupled and the kernel tries very hard to only do as much as it needs to. For commonly-accessed drivers, for example, an IPC round-trip requires only a selector switch (which a macrokernel OS does anyway when it enters and exits kernel mode) and avoids the address space switch completely.
Of course, none of this applies to Mach, which isn't a "micro"-kernel by modern standards.
On the P4, the expensive part was entering and exiting kernel mode; it even dominated address space switching and TLB reload for typical scenarios. I don't know about modern CPUs, but the key point remains: "extra context switching [...] kills performance" is a claim that's hard to prove.
FTFM
High frequency trading systems are not a typical example of anything, and should be held as a typical use case for any reasonable operating system. They do things like use custom network hardware which plays fast and loose with the standards, and could easily be compromised if they weren't on a fairly trusted network.