microarchitect · HackerTrans

microarchitect

no profile record

投稿

Using SMT Solvers to Analyze the Premier League Table

spramod.info

56 ポイント投稿者 microarchitect11 年前4 コメント

End-to-end analysis of the spam value chain [pdf]

cs.princeton.edu

1 ポイント投稿者 microarchitect14 年前0 コメント

Is aggregate data always private?

techatftc.wordpress.com

1 ポイント投稿者 microarchitect14 年前0 コメント

Shared Memory Consistency Models: A Tutorial [pdf]

rsim.cs.illinois.edu

2 ポイント投稿者 microarchitect15 年前0 コメント

How Gene Marks Could Have Done Better

isisthescientist.com

1 ポイント投稿者 microarchitect15 年前0 コメント

Attaboy: Not standard HN Fare, but I really believe hackers will appreciate this

youtube.com

1 ポイント投稿者 microarchitect15 年前0 コメント

Arvind Gupta's toys

arvindguptatoys.com

2 ポイント投稿者 microarchitect15 年前2 コメント

AMD withdraws from Sysmark 2012

blogs.amd.com

1 ポイント投稿者 microarchitect15 年前0 コメント

コメント

11 年前議論

Something a lot of bitcoiners don't seem to realize: the security of a blockchain is entirely due to the fact that it is too expensive to attack it. If your blockchain is "secured" by a motley bunch of ragtag microcontrollers, the first guy to point an ASIC at this chain can 51% attack it willy-nilly and render the blockchain useless.

PS. This is not a theoretical statement. It has happened to numerous altcoins.

PPS. In case it needs spelling out, the fact that its too expensive to attack the blockchain means that it is even more expensive to secure it (because miners need to make a profit).

11 年前議論

How good is the compiler? To paraphrase David Patterson, its easy to get really great IPC for code from a shitty compiler, but that doesn't mean your program will run faster.

11 年前議論

There's been a few different proposals to use functional languages to write hardware: Chisel (https://chisel.eecs.berkeley.edu/) and Bluespec (http://www.bluespec.com/) are two others. They haven't really taken off because the productivity bottleneck in hardware is not in design but verification and specifically sequential verification. Combinational verification is quote easy, because modern SAT solvers can prove almost all combinational properties you can throw at them.

The trouble comes in when you start dealing with complex state machines with non-obvious invariants. I don't think these functional languages can really help too much here because unlike C or C++ in the software world, there isn't unnecessary complexity introduced by a language, e.g. verification becoming harder due to aliasing. It's the properties themselves that are complex. Lots of progress is happening though: Aaron Bradley's PDR (http://theory.stanford.edu/~arbrad/) and Arie Gurfinkel and Yakir Vizel's AVY (http://arieg.bitbucket.org/avy/) have made pretty major breakthroughs in proving a lot of complex sequential properties and these algorithms have made their way into industrial formal tools as well.

11 年前議論

It's definitely colonialism and the effect of modern western media.

I know this because I grew up seeing this change happen in India. Today in India everyone (obviously an unfair generalization but still) wants to conform to the white standards of beauty. This wasn't always the case. In south india, I gradually saw the change happen; each generation of film actors was more light-skinned than their predecessors.

And if you read the classics of Indian literature, a lot of the protagonists are dark skinned. The funny thing is even a lot of the Indian gods and mythological characters are portrayed as being dark skinned in the myths, but modern paintings, TV serials and movies portray these characters with light-skinned actors!

11 年前議論

I'm not sure if I understand what you mean by accuracy. This is not a probabilistic analysis. The solver considers the space of all possible outcomes for each match and returns satisfiable if there is some set of outcomes that satisfies the constraints. For example, it says that Stoke City can still qualify for the CL, but this requires that all of the current top 4 will need to pretty much lose every match while the teams below them win every match. This is obviously so unlikely to happen that you might as well disregard it it, but it is still a mathematical possibility and so the solver returns satisfiable.

As far as la liga is concerned, yes, you can definitely do a similar analysis. You will have to change the code that calculates the league positions, because in la liga if two teams are level on points then the first tie-breaker is head to head record, and then goal difference if the head to head is also equal. This should be a pretty straightforward change.

11 年前議論

Honestly, 8/16b ints in C and C++ are just a minefield of problems.

Here's a snippet from an open source 8051 simulator that I was debugging today:

        if( ((RAM[ACC] & 0xF0) >> 4) > 9 || 
            GetBit(RAM[PSW], CY) == 0x01 ) {
            tempAdd = RAM[ACC] + 0x60;
            RAM[ACC] = tempAdd;
            if( ((unsigned char*)&tempAdd)[1] != 0 ) {
                SetBit(RAM[PSW], CY);
            }
        }

The code is supposed to set the carry flag when RAM[ACC] + 0x60 overflows into two bytes. Can you spot the bug? It involves my favorite C++ feature: implicit conversions, and my second favorite feature: signed chars.

The bug is that when RAM[ACC] is something like 0xFF, it gets cast to (int) -1 so the the upper byte and hence the carry flag never get set.

I predict there's lots more more evil that can milked from this fount.

11 年前議論

I am not the OP, but I'm using Z3 in my research to help with the formal verification of hardware and firmware.

My problem is as follows. I have a microcontroller which runs firmware. I want to verify various things about the hardware+firmware combination. For instance, I may be interested in proving that user mode firmware cannot change the MMU configuration.

There are many parts to this problem. First is verifying that the kernel doesn't expose routines that let you do these kinds of things. This is a kind of s/w verification problem, somewhat well studied. Second, you want to make sure there are no h/w bugs in the microcontroller itself which the user mode software can exploit to do bad stuff. This is traditional h/w verification, also well-studied. The third is that there aren't weird corners of the microcontroller ISA specification itself which can be exploited. This is also a kind of h/w bug albeit a specification bug.

The third part is where Z3 comes in because often, there isn't any specification, and if there is, it's a bunch of PDFs or word documents. What we want is to generate a formal specification, which you can examine using formal tools to prove that it satisfies certain properties. And then we want to prove that our implementation conforms to this specification. We're using some techniques from program synthesis with Z3 as the solver for this.

12 年前議論

This is the #1 reason why I won't stay in the US after my phd. I have no interest in being a random CEO whim away from either having to uproot my life and move back home or frantically try to land a new job all in the short period of 15 days.

For those curious the #2 reason is that H1Bs make it hard to do even simple extracurricular activities like writing books or do consulting on the side related to an open source project you contribute to let alone start a company.

The H1B is fundamentally broken and I'm amazed that so many people put up with it. Credit to the US for being such a desirable destination, I guess.

13 年前議論

You have way too much time on your hands if you are considering review requests from people you don't know.

13 年前議論

What makes a conference good isn't the IEEE label but rather the reputation of the conference itself and its corresponding ability to attract a high quality program committee.

The important point here is that there isn't a shortcut to evaluating conference quality. You have to know your field, know who is worth listening to and who isn't, know what the top conferences are, what the mediocre conferences are and so forth. If a new conference springs up, you need to be able to judge whether to pay attention by looking at the PC.

> Of course there are regional IEEE conferences. But in general, the international IEEE conferences and journals by the bigger societies are probably the best ones out there.

You can't really make general statements like that. For example, CAV proceedings are published by Springer (http://www.springer.com/computer/theoretical+computer+scienc...). JPDC is a well-regarded journal in the parallel computing community that is published by Elsevier.

And a "regional" conference doesn't mean it's a bad conference. DATE (http://www.date-conference.com/) is probably the second best design automation conference behind DAC. ASPDAC, ATVA, APLAS, FSTTCS are some well-regarded regional conferences and there are plenty more like these. Not all of these are IEEE sponsored either.

> I have published quite a bit in the physical sciences/engineering field and in my experience the IEEE journals have a far better peer review process than AIP, ACS, Elsevier and even NPG. The same goes for the conferences.

I'm not trying to slight IEEE here. I looked through my publication list and it turns out all my papers are in IEEE conferences and journals! But on the other hand, a few of them could easily have ended up in a venue like CAV and this wouldn't magically make them worse papers.

The key point here I want to make here is this: there is no substitute for knowing your field, if you're judging conference quality by the IEEE label, you're doing something wrong.

13 年前議論

The IEEE label isn't an indicator of quality and similar papers have been published in IEEE sponsored conferences. See http://diehimmelistschoen.blogspot.com/ and http://pdos.csail.mit.edu/scigen/.

One of my old professors used to joke that "for every paper, there is a conference that accepts it." Unfortunately this is somewhat literally true. This isn't unique to any one country as the SCIgen successes demonstrate and I don't really see a solution to it.

13 年前議論

I was in Bangalore some weeks ago and I tried the query "OK google, directions to vidyarthi bhavan." And it worked perfectly. I was amazed!

The first thing that amazed me was that Google understood what I meant by vidyarthi bhavan! Note vidyarthi bhavan is a generic phrase in many Indian languages which just means 'student building.' In Bangalore, it refers to a specific restaurant in Gandhi Bazar famed for its masala dosas. And I bet there are plenty of people who live in Bangalore right now and don't know about this restaurant. The contextual knowledge here is amazing. And it wasn't just geolocation, I was about 15km away from Gandhi Bazar at that point. And Bangaloreans will know corresponds to an eternity given the traffic situation. And the software did all this by recognizing a phrase consisting of two words, both of which are not in English!

That moment was an epiphany for me, it the precise moment that I realized that personal digital assistants are here, and they actually work.

13 年前議論

What they are missing is that it's not performance per watt, but performance per watt per dollar.

Intel may be able to build lower power/faster chips but their foundries aren't cheap, neither are the thousands of engineers Intel puts on each SoC, and technology scaling is only getting more and more expensive.

It's a classic case of the innovators dilemma. Intel are optimized to sell very fast chips that cost hundreds of dollars but the performance of fast-ish chips that cost a few dollars has almost caught up to them and Intel simply can't compete without a complete restructuring. A further complicating factor is the fact that ARM is a weird many-headed chimera [1] that Intel simply can't kill they way the did with x86 competitors like AMD.

[1] http://www.anandtech.com/show/7112/the-arm-diaries-part-1-ho...

13 年前議論

Although SAT is indeed NP-complete, modern solvers are ridiculously fast for the kinds of SAT queries that appear in scenarios like hardware model checking and verification. It's not uncommon for queries with millions of variables and clauses to be solved in a matter of seconds. There are some algorithmic tricks combined with clever data structures and search space exploration heuristics that make this possible.

btw, if you're curious about the workings of a modern SAT solver, the first few sections of this paper: http://www.georg.weissenbacher.name/papers/mod12.pdf should make interesting and hopefully accessible reading.

Unfortunately, I don't know enough about the internals of Z3 to know what specifically makes it the fastest SMT solver. But I also don't think it's too far wrong to say that SMT solvers like Z3 are fast because the underlying SAT solver they use is very fast.

13 年前議論

In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving.

If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394. To make a long story short, various problems in program verification and static analysis have seen success with SMT.

/some academic navel-gazing follows.

Yices (http://yices.csl.sri.com/index.shtml) and Z3 are the two main SMT solvers used by academics today. Yices is the "original" solver and was developed by Leonardo de Moura and Bruno Dutertre at SRI in the mid-2000s. At some point towards the end of the last decade, Leonardo moved to Microsoft Research and for reasons which are unclear started working on Z3 independently. I am told that Z3 is a slightly faster solver today.

13 年前議論

Some thoughts on this issue. Some of these have been expressed by others like pg already.

1. Workers are not a commodity and not interchangeable. You can't a take a network-layer programmer who got laid-off from Cisco and ask that person to work on big data and reasonably expect success.

2. I suspect a lot of tech workers are not motivated by money as long as it's above a threshold. I know for a fact that I've taken jobs that paid me as much as 25% less because I got to work on "cooler" stuff. This also fits in with the stories of Google's early days when they actually paid less in dollar terms than MS but were able to lure workers away from MS because they had better "perks" and more interesting technology.

2a. If progammers were optimizing for money, most of us would be working for wall Street, and we'd all be contracting in our free time instead of building open source apps. Clearly this isn't happening.

3. Anecdotally, I know for a fact there is huge demand for competent programmers/engineers because I have standing offers from multiple employers. The reason for this is that a good programmer is orders of magnitude more productive than an average programmer so good managers will move heaven and earth to get their hire. On top of this, an average programmer in a good team will have effective negative productivity. So restricting your supply pool even a little bit can leave you with a drastically less productive team.

13 年前議論

Thanks for that that those very interesting links. But I still don't think that is what is going on here.

In designs which rename using the ROB, the register file holds values produced by instructions which are completed and retired, the ROB holds values from instructions that are completed but not retired, and the bypass network supplies values from instructions currently completing.

What Agner is doing in his example with the seemingly useless instruction is transferring a value from the the register file to the ROB so that instructions which try to read logical register ECX will now source it from the ROB instead of the register file. But when I look at the code in the stack overflow question, nothing actually reads from s1. So these are even "more useless" instructions than Agner's example.

Some people have already mentioned instruction alignment issues, so that is one likely explanation. There are a whole bunch of other possible issues involving the scheduler and dispatch restrictions. For example, I've seen processors where there were two pipelines with slightly different instruction schedulers. So adding a useless instruction like this might push your bottleneck instruction into a pipe with a scheduler that is slightly better for your code. Sometimes bypassing across different pipes is more expensive than within the same pipe, so again the useless instruction might push some instructions into pipes that have more of their sources. It could one of any number of reasons and it's going to be very hard to tell from the outside without knowing the details of the microarchitecture.

13 年前議論

Sorry, this explanation is almost surely incorrect. How long something is available on the bypass network is determined by how long the instruction that produces the value takes to "exit" the pipeline. I can't imagine any scenario where a consumer instruction causes a producer instruction (i.e., an instruction "ahead" of it) to stall. Note this would be a dangerous design point because of the risk of deadlocks.

What's the source for your claim that the Core uarch's register file is underdesigned in comparison to the dispatch width? I'd be extremely surprised if this were the case. Last time I looked at the data, about 50-70% of the reads go to the register file not the bypass network.

13 年前議論

Deeper pipelines have higher clock frequencies but this comes at the cost of lower instructions per clock (IPC). Roughly speaking, asking for a shallower pipe essentially boils down to asking for a lower clock frequency. Deeper pipelines are more complex to build, tricky to validate, not to mention the obvious fact that they consume more area and power, so architects who choose deeper pipelines are doing so only because performance studies show that these pipes are worthwhile.

The branch in this example is essentially random and so pretty much impossible to predict. I would classify it as a pathological case. A modern predictor such as perceptron [1] or even the older tournament predictor [2] is extremely accurate for branches found in real benchmarks.

[1] http://www.cs.utexas.edu/~lin/papers/hpca01.pdf [2] http://www.hpl.hp.com/techreports/Compaq-DEC/WRL-TN-36.pdf

PS. Sidenote about the P4, it achieved the highest SpecINT CPU score among all its contemporary processors so it wasn't the performance disaster some people make it out to be. It's worth noting that SpecINT CPU is has traditionally been the most challenging benchmark in terms of branch prediction requirements. SpecFP CPU for example is full of easy to predict loops.

13 年前議論

Overstaying on an F1 visa is quite hard because the school is required to report all changes in academic status through the SEVIS database.

If you want to stay and work go through the proper legal process and get a resident visa.

F1 students are allowed to work 20 hours a week when the school is in session and 40 hours a week during the summer.