Category: systems

  • A claimed validated operating system.

    The claim: we have demonstrated the comprehensive formal verification of the seL4 microkernel, with a complete proof chain from precise, formal statements of high-level security and safety properties to the  binary executable code. GD The L4 base is useful –  we advocated a similar approach with RTLinux which was, um, very similar to L4. It…

  • Cassandra

    Cassandra is quite interesting – and time sync seems increasingly critical to correct operation. Here are some resources: A paper on the storage model from developers at Facebook. A reasonably clear introduction from IBM Developer Works. A big difficulty for people who are, like me, more familiar with the relational databases is that Cassandra and…

  • Real-time Linux

    My opinion has always been that the Linux-RT project was based on an unfixable engineering error.   A few words on the status and the future of RT: ———————————————– The situation since last years RTLWS (https://lwn.net/Articles/572740/) has not improved at all, it’s worse than before. While shortly after RTLWS quite some people promised to whip…

  • A basic design error in software

    Suppose we didn’t know too much about bridge design, but were convinced that (a) the current design methods were too slow and unmodular to be useful, and (b) not knowing anything about structure other than what we could observe of completed bridges was no barrier to coming up with a new method. We might start…

  • Obama’s big data team

    Those applications used a huge chunk of Amazon’s Eastern data center. “We had thousands of nodes,” said VanDenPlas. “We pushed 180TB of traffic with billions and billions of requests. We had 60% of all of Amazon’s medium [instances] in US East.” Read more: http://sdt.bz/37299#ixzz2I0RN4r00

  • Big Data and politics

    For the general public, there was no way to know that the idea for the Parker contest had come from a data-mining discovery about some supporters: affection for contests, small dinners and celebrity. But from the beginning, campaign manager Jim Messina had promised a totally different, metric-driven kind of campaign in which politics was the…

  • Free Software Patents: Alan Cox

    1. A method, comprising: storing, by one or more processors, confidential data in a confidential section of virtual memory, wherein storing the confidential data in the confidential section of virtual memory comprises: mapping the confidential section of virtual memory to an address space in a first physical memory device; storing the confidential data in the…

  • Julia programming language and hadoop

    While we’re being demanding, we want something that provides the distributed power of Hadoop — without the kilobytes of boilerplate Java and XML; without being forced to sift through gigabytes of log files on hundreds of machines to find our bugs. We want the power without the layers of impenetrable complexity. We want to write…

  • Apple’s A5 chip made in Austin

    Although I think it might have been designed here too. The A5 processor – the brain in the iPhone 4S and iPad 2 – is now made in a sprawling 1.6 million square feet factory in Austin owned by Korean electronics giant Samsung Electronics, according to people familiar with the operation. One of the few…

  • Droning on about computer security

    Good grief. The US military’s unmanned Predator and Reaper drones are continuing to fly remote missions overseas despite a computer virus that has infected their US-based cockpits. Government officials are still investigating whether the virus is benign, and how it managed to infect the heavily protected computer systems at Creech Air Force Base in Nevada,…