xgk
When it was created, PyPy did not seek to optimise startup performance. Instead, its aim was steady-state performance of JITed code, and it succeeded handsomely. A conceptually simple fix would be to optimise traces in one processor core, while the interpreter runs in another. Once when the trace is finalised, does interpretation stop and switch to native execution. But PyPy is currently a sequential system and making it parallel, while conceptually easy, is a lot of work and needs a rewrite of the whole system. But, for better or worse, the PyPy team does not have the resources to do this.
The other of PyPy's big performance issues (Python code using a lot of FFI calls via a suboptimal FFI) is also, in principle, easily fixable. But this is a social problem: the Python community would have to move towards better FFIs.
In principle, it would also be easy to fix PyPy's resource problem. I am not sure about the social problem ...
[1] R. A. Jacobs, M. I. Jordan, S. J. Nowlan, G. E. Hinton, Adaptive mixtures of local experts. (1991)
[2] M. I. Jordan, R. A. Jacobs, Hierarchical mixtures of experts and the EM algorithm. (1993)
[3] L. Xu, M. Jordan, G. E. Hinton, An alternative model for mixtures of experts. (1994)
[4] S. Waterhouse, D. MacKay, A. Robinson, Bayesian methods for mixtures of experts. (1995)
[5] N. Shazeer, A. Mirhoseini, K. Maziarz, A. Davis, Q. Le, G. Hinton, J. Dean, Outrageously large neural networks: The sparsely-gated mixture-of-experts layer. (2017)
x
x._polynomials_gf_2
> You do not need another language for this.
By the Church-Turing thesis you never need another language, but empirical practise has shown that the software engineering properties we see with real-world code and real-world programmers differ significantly between languages.
One interesting programming language construct that might be useful in this context are Opaque Type Synonyms which modern languages like Rust, Haskell, Go or Scala offer. This allows the programmer to use the same underlying types (e.g. int), give it different names, and define different algebras with the alias. The typing system prevents the different aliases accidentally to flow into each other.
Yes, that's true, but the registers themselves are untyped, what modern CPUs really implement is multiple instruction semantics over the same bit-patterns. In short: same bits, five algebras! The algebras are given by different instructions (on the same bit patterns).
Here is an example, the bit pattern 1011:
• as a non-negative integer: 11. ISA operations: Arm UDIV, RISC-V DIVU, x86 DIV
• as an integer residue mod 16: the class [11] in Z/16Z. ISA operations: Arm ADD, RISC-V ADD/ADDI, x86 ADD
• as a bit string: bits 3, 1, and 0 are set. ISA operations: Arm EOR, RISC-V ANDI/ORI/XORI, x86 AND.
• as a binary polynomial: x^3 + x + 1. ISA operations: Arm PMULL, RISC-V clmul/clmulh/clmulr, x86 PCLMULQDQ
• as a binary polynomial residue modulo, say, x^4 + x + 1: the residue class of x^3 + x + 1 in GF(2)[x] / (x^4 + x + 1). ISA operations: Arm CRC32* / CRC32C*, x86 CRC32, RISC-V clmulr
And actually ... the floating point numbers also have the same bit patters, and could, in principle reside in the same registers. On modern ISAs, floats are usually implemented in a distinct register file.
You can use different functions in C on the bit patterns we call unsigned.
Are China's demographics appreciatively different from other industrialised countries? Questionable. Not to mention that it's unclear why an aging society is a problem at least for the next 100 years or so (e.g. most violent crime is perpetrated by the under-30s). It's also easy, at least for a dictatorship, to increase the birth rate (e.g. restrict access to all birth control, give massive preferences to families with children, like housing, salary, "bachelor tax" etc).
> military containment of China.
That is expensive. One frequently cited explanation for the collapse of the Soviet Union was that its poor economy could not support its oversized army, which it needed to keep the Soviet Bloc at heel (not to mention all the revolutions and secession movements it fostered elsewhere).
Also, does anyone actually believe that China is expansionist? Compare:
https://en.wikipedia.org/wiki/List_of_wars_involving_the_Uni...
https://en.wikipedia.org/wiki/List_of_wars_involving_the_Peo...
The strategic problem of China's rise is more that other countries will eventually switch allegiance away from the West.
And not just companies. This is currently the world's top open-source RISC-V development https://github.com/OpenXiangShan coming from the Chinese Academy of Science.
(Whether China will remain investing in RISC-V, given that the US government has started to pressure US RISC-V development to limit their involvement with China is another question.)
1. Stopping technology transfer worked exceedingly well for the west weakening the Soviet Union during the Cold War.
2. A distinct lack of (non-violent) alternatives for the West preventing China becoming the world's leading technological superpower (and hence also strongest military).
I doubt this will be successful in the long run, because China is not burdened by the Soviet Union's extremely inefficient way of organising its economy. Not to mention that China is the worlds biggest market.
I recommend [1] as an introduction to the semiconductor physics behind the Rowhammer problem. Rowhammer is an instance of the "weird machine" problem behind many security problems, i.e. a mismatch between two abstractions: the abstraction we pretend describes the system, vs the reality of the system. In the case of Rowhammer, that is the abstraction of memory as a digital device, against the reality of storing bits with capacitors and wires, ie. analog devices. Clearly a leaky abstraction. The denser you pack those capacitors and wires, the more leaky.
[1] A. J. Walker, S. Lee, D. Beery, On DRAM Rowhammer and the Physics of Insecurity. https://ieeexplore.ieee.org/document/9366976
As silicon density increased, the issue became more urgent.
I don't believe that Rowhammer mitigations happen inside the DRAM chips themselves, I think that they are being put into the memory controller that talks to DRAM. Since DRAMs with built-in Rowhammer defences would have to spend transistors on this defence, those transistors would be 'wasted' in situations where Rowhammer is not part of the attacker model.
On one side ...
On the other side ...
questionably from the beginning
I wonder which cloud provider is the first to offer this in a coherent way.
studies are bs because
- a better empirical grounding of programming language & software engineering research;
- more emphasis on reproducibility in science.
I'm glad that Vitek, Berger et al are starting serious empirical PL/SE research, and care about reproducibility! Bravo!
somehow messed with Cs
absorption line
As far as I can see, measuring time is the foundation of all definitions of other units. And the core reason why time is used to define everything else, is pragmatic: it's just technically easier to count (photon absorption) than to do anything else.
[1] https://en.wikipedia.org/wiki/2019_redefinition_of_the_SI_ba...
precisely known transitions
True, and with program logics, you can choose partial correctness vs total vs generalised correctness.
Itt's even worse in practise. With many contemporary dependently typed languages you'll have to worry about termination even during programming, even before thinking about verification.
The Curry-Howard prover advocates seem to regard this as a solved problem ("just distinguish programs from proofs by way of a typing system, problem solved") but has this solution been implemented in any mature systems as of 2017?
Exactly.
Program logics are superior in this regard: the encourage rather than inhibit separation of concerns. (Not to mention: program logics are more developed and cover a large class of computing paradigms, while dependent types have not grown much beyond the pure functions ghetto.)
I put forward this point to dependent types luminaries all the time. Its difficult to get more than polite silence in response.
* * *
- As an undergraduate writes a lambda-calculus interpreter in Lisp/Scheme/Racket/Haskell
- As a PhD Student writes their own pure language with wacky typing system, and demonstrate its usefulness by embedding a lambda-calculus interpreter in it.
- As a postdoc verifies a lambda-calculus interpreter in Coq/Agda.
- As an assistant professor writes their own Curry-Howard-based interactive prover in some dependently typed language and demonstrate its usefulness by verifying a lambda-calculus interpreter in it.
- After tenure, gets their students to do the above.
2018's POPL has a type-theory in type-theory paper, but none on how programming language theory can improve SAT solving ...
It's an echo chamber. I recently reviewed a grant proposal by some of the more famous dependent types researchers. They proposed using HoTT to verify computational effects. The grant proposal claimed (1) that there is currently no known way to verify effectful languages and (2) that embedding generalisations of effect monads in HoTT is the way to overcome this problem. It seems like these people have not ever heard of program logics?
* * *
The real problem is automation.
Better autmation means dramatically better SAT solvers (modern SMT solvers are heavily reliant of SAT solvers). It's just unclear where 10x, 100x, 1000x speedups in SAT solvers should come from. We don't even know how to parallelise SAT solvers well. In the absence of dramatic progress in SAT solvers, what can we do other than tinkering with dependently typed languages and their relatives?
melody, harmony, and rhythm [...] timbre
To be fair meaning is extra-musical, and varies between listeners.
Other than that, you are absolutely correct: timber is the focus of modern electronic music. All previous genres simply lacked the instruments to do much of interest in the way of timber.
May I ask what is on-topic on HN these days?