Several years after the dot-bomb, I finally realise what all of the fuss was about with regard to Aeron chairs. I am currently visiting The University of Utah to collaborate with a researcher here and today I replaced the default chair I was using with an Aeron chair from an unused office. It is incredibly comfortable, and made even better by the fact that my supervisor doesn't have one.

On the more geeky side, there are a couple of large SGI SMP boxes (one 60 CPU, one 30) for me to play with and a Linux cluster.

Today we warned the technicians that we might need to use a big chunk of disk space. We were told that there might not be enough, since they only had about 200GB free on the RAID array we wanted to use (the one local to the 60 CPU box). Back home, our technicians complained when I dumped a 2GB DVD image in my home directory...

Sometimes ideas don't get the attention that they deserve. The Java Modelling Language (JML) is just such an idea. JML is something every Java programmer should know about. That does not mean every project in Java should make use of JML, only that developers should be aware of it so they can use it wherever it does make sense. The fact is that JML provides so many benefits for so little extra work that it deserves far more use than it gets. If you program in Java it could make your life a lot easier.

What is JML?

In a sense JML is just a way to document your code better. JML provides simple intuitive syntax to provide concise descriptions of behaviour in a Java module. JML uses annotations to document all the mundane things you would normally document. For example you might want to note which fields are allowed to ever be null, or whether a particular method requires one of its parameters to be greater than zero, or if a method is side-effect free. What JML really offers, however, is the tools to make use of these extra comments to save you time and effort later. JML simply asks you to do what you would normally do, and in return offers improved productivity when it comes to documenting, testing, and debugging your code.

So what exactly does JML look like? Here's a simple toy example that, while contrived, manages to demonstrate a lot of basic JML and will be useful later for demonstrating what tools that use JML can do.

public class Example {
 
    public int modifiable = 0;
    private /*@ spec_public @*/int additional_value = 5;
    private /*@ spec_public non_null @*/ String current_substring;
 
//@ invariant additional_value >= 5;
//@ invariant current_substring.length() == modifiable;
 
//@ requires ((String) o).length() > modifiable;
//@ assignable current_substring;
    public void castExample(/*@ non_null @*/ Object o) {
        additional_value = o.hashCode()%5;
        current_substring = ((String) o).substring(0, modifiable);
    }
 
//@ requires x >= -5;
//@ ensures \result > 0;
    public /*@ pure @*/ int pureFunction(int x) {
        return x + additional_value;
    }
 
//@ assignable modifiable;
//@ signals (ExampleException e) additional_value <= 4;
    public void unreachable() throws ExampleException {
        if (additional_value > 4 && modifiable > 0) {
            modifiable++;
        }
        else if (modifiable == 0) {
            throw new ExampleException();
        }
        else {
//@ unreachable;
        }
    }
}

Most of the JML annotations should be clear: We are simply documenting constraints on inputs (requires clauses) and outputs (ensures clauses, noting when fields or parameters cannot be null or when code is (we presume) unreachable, and what invariant properties that we expect the objects to have. A little less immediately obvious are the assignable and signals clauses. An assignable clause declares what is allowed to be written/assigned to from within the method, and a signals clause declares conditions that must be met in the case of an exception being thrown. Finally spec_public simply declares that these private fields have public visibility to the specification. You may note a few errors where the specification and the code don't agree - we'll come to those shortly.

This is, of course, only a small sample of what JML offers. JML provides a lot of useful syntactic sugar to make stating your intentions as easy and natural as possible. For a proper introduction to JML there are some presentations on basic JML and more advanced JML. Full documentation can be found in the JML Reference Manual.

What do I get out of it?

JML provides an easy to use language with which you can concisely say how you intend your code to behave. More importantly it provides tools to make full use of that. For the small amount of extra effort of documenting your intentions with JML you get a lot of easy gains.

The JML tools

The JML distribution comes with a number of tools that use JML annotations. The four most useful are jmldoc, jmlc, jmlrac, and jmlunit. The first, jmldoc performs the same function as Javadoc, producing almost identical API documentation. The advantage of jmldoc is that it understands JML annotations and includes suitable extra information in the API documents based on the annotations. As long as you document requirements and guarantees for modules in JML you can be sure that the API documentation will always include those constraints. Furthermore because JML annotations become integral for testing and debugging it is far more likely that the annotations are kept up to date with the code, meaning that documentation is also more likely to be up to date.

The tools jmlc and jmlrac provide a JML aware compiler and runtime environment. The advantage of compiling and running code with such tools is that JML annotations are converted into assertions which are checked at runtime, making it easier and faster to discover and locate bugs. For the small cost of writing a few annotations you can significantly speed up the testing and debugging cycle.

You can get the similar results by liberally sprinkling assertions through your code, but JML offers several advantages over such a scheme:

1. JML provides a lot of syntactic sugar like universal and existential quantifiers (\forall and \exists), and logical connectives like "implies" (==> ) and "if and only if" ().
2. JML elegantly handles inheritance. When overriding a method you will have to rewrite all your assertions, while JML annotations are automatically inherited. If you want to add annotations to those inherited by an overridden method JML provides the also keyword.
3. As JML annotations are comments, and only converted into runtime assertions when you use the jmlc compiler, turning off runtime checking is as easy as compiling with a standard Java compiler. Using assertions will have you jumping through hoops to arrange anything similar.
4. JML annotations can be automatically included into your JavaDoc documentation. If you use assertions you'll have to repeat the information elsewhere to get it included in the documentation

Of course having assertions based on intended behaviour is no substitute for a decent unit testing framework. JML has an answer for this too however. The jmlunit tool can read a Java module with JML annotations and automatically generate a JUnit test class based on the annotations. For example running jmlunit over our example above creates two new files Example_JML_Test.java and Example_JML_TestData.java. The first of those files is a JUnit test suite, and the second is used to generate test data. JML attempts to come up with a reasonable test data generation strategy, but leaves space for you to enter your own set of test data instead should you prefer.

Extended Static Checking

Extended static checking is where JML annotations begin to truly come into their own. ESC/Java2 is an extended static checking tool for Java that uses JML annotations to catch errors before you even compile, let alone run, the code. You can think of it as type checking on steroids - using the information in the annotations to warn you about a wide variety of potential errors. It runs about as fast as compilation, so there's no waiting for results.

Consider what happens when we run the example above through ESC/Java2. We get a series of warnings (some not revealed until others have been corrected):

1. We are warned that current_substring is uninitialized and could be null
2. We are warned that additional_value is modified when it shouldn't be (line 14)
3. We are warned that the cast made in castExample may be invalid
4. We are warned that the postcondition for pureFunction may be violated (it's possible that x = -5 while the invariant only ensures that additional_value is at least 5, thus 0 could be returned).
5. We are warned that an exception may be thrown in unreachable without the conditions being met
6. We are warned that the //@ unreachable portion of code is, in fact, reachable
7. We are warned that the invariant current_substring.length() == modifiable can be violated.

Most of the errors listed above are either errors in code, or in our expectations of what the code will do. Some of these errors can be remedied by strengthening the constraints. For example we can add //@ requires o instanceof String to castExample to fix the warning, but at the cost that any code calling that method must meet that precondition (though the API documentation will state the precondition). Other errors can only be corrected in the code itself.

While the errors are necessarily simple in this toy example, hopefully this gives you the flavour of what ESC/Java2 can do for you - it has very powerful algorithms and scales to remarkably complex code, easily finding errors that would be hard to spot by inspection. For more examples of what ESC/Java2 can do for you (and it is well worth reading) try this introduction to ESC/Java2. ESC/Java2 offers a robust and powerful tool for finding subtle errors in your code earlier when they are easier to fix.

Conclusions

JML is simple to use: it has an expressive and intuitive syntax, and you can write the annotations at the same time the code. JML is also flexible: you an use as much or as little in the way of annotations as you need. Perhaps you simply want to add some pre- and post-conditions, or just keep track of which methods can access or alter certain fields; perhaps you want to use the full power of the theorem provers in ESC/Java2. Most of all JML makes many aspects of development, from debugging and testing to documenting, easier and more efficient, all for very little extra effort. If you program in Java for a living then JML can almost certainly make your code better, and your life easier.

There have been a lot of arguments recently about why OS X sucks for some things, and the blame is often laid at the door of OS X's threading performance. This seemed odd, since OS X gets its threading system from Mach, which was designed to support threading from the ground up. As it turns out, the reason is somewhat more subtle.

OS X sucks at system calls. Due to the Mach+BSD kernel design, system calls are very expensive on OS X. On Mach, the system call cost is around 10x the cost on BSD - on OS X it's some combination of the two depending on what you do. The next thing to realise is that all of the POSIX thread synchronisation mechanisms are implemented using Mach-level synchronisation primitives. This means every time you lock a mutex (for example) you need to dive down through the BSD layer to the Mach layer. This gives you the horrible overhead of checking the permissions on a Mach port (something that sane Microkernels like L4 abandoned), and is expensive. This makes locking operations on OS X much more expensive than on BSD-like kernels. This, in turn, can make threaded code much slower. If you are Adobe, and you are rendering an entire image transformation in a small number of threads, then you will only lock at the beginning and the end of the operations, so it will be nice and fast. If you are doing low-level parallel operations for scientific computing (when not bitching about the OS X kernel), then you should really try harder to persuade someone to buy you a nice Solaris box.

Today, I wrote some code that enumerates, at run-time, all of the classes which conform to a particular protocol (that's implement a given interface, for any Java programmers) and allows the user to select one.

This is why I like Objective-C, and why using languages like C++ feels so painful in comparison. Oh, and for reference, enumerating the classes was around half a dozen lines. Sure, this kind of thing is possible in C++, but only if you build a huge amount of extra stuff on top.

I have recently become interested in the concept of open source hardware. It seems that you can buy FPGAs which provide a reasonable amount of performance for a relatively low cost. This means that you can implement your own CPU etc. designs in Verilog / VHDL. Places like opencores.org allow collaborative work on these designs, and so you can even download someone else's CPU design and use this.

This is all well and good, but FPGAs don't offer the same feature density as even ASICs (although they are re-writable), so this raises the question of whether it would be commercially viable to do a run of ASICs based on an open core, with a motherboard also based on an open design. Would you buy a motherboard / CPU that could run, for example, NetBSD and was entirely open source? How much of a premium would you be willing to pay for such a thing?

I really like the design of the Alpha CPU, and I would be interested in a machine that had a similar core design, and maybe willing to pay around a 50% premium over x86 for the elegance of the system - particularly if I could also download the core design to an FPGA, modify it, and submit changes back for inclusion in the next revision.

One of the real advantages of open source software is that it can easily be compiled for multiple architectures, so once you've written a GCC back-end and a boot loader for your system you suddenly have a huge amount of usable software.

I am rapidly coming to the conclusion that the ideal CPU would have a very simple instruction set, and not even do out-of-order execution. Code running on it should be compiled first into some kind of byte-code, and any re-scheduling should occur in the bytecode JIT - move as much complexity into software as possible, since it's much easier to upgrade (and to configure at run-time).

This time it's my coverage of Linux 2005 making Slashdot and my Project Evil Tutorial on OSNews. Nice - and I'm very glad I'm not the server admin - the new server is running UML, and hasn't been Slashdot-tested yet.

Formal Specification helps build more robust, more maintainable software with fewer bugs and defects. It has a long history, but it is still a developing field. While it may not be suitable for all software projects, a case can be made that there are many projects not currently using formal specification that stand to benefit from it. As the methods and tools for formal specification develop it is increasingly becoming something that developers and software engineers should learn to use to their advantage.

What is Formal Specification

Formal specification is simply a matter of being more explicit and specific in defining the requirements of software. At the simplest level this can take the form of Design by Contract, where functions and procedures specify pre- and post-conditions and loops and objects include a set of invariant properties. In the more rigorous case formal specification involves building an explicit mathematical definition of the requirements of the software. Using such a definition one can prove the correctness of the system, or simply prove theorems about properties of the system. An implementation can also be checked against such a formalised specification, verifying that the implemented code does indeed do precisely what the requirements claim. At the most rigorous level the initial formal requirement specification can be expanded, through (mathematically rigorous) refinement, to ever more specific and detailed specifications resulting eventually in executable code.

All of these different levels allow a significantly greater degree of analysis of the software, be it improved static and runtime checking with contracts, to more complex data flow analysis and proof with more complete specifications. In the same way that static types allow more rigorous checking at compile time, catching a lot of simple errors, contracts and specifications allow even more analysis and checking, catching even more errors at the early stages of development when they are most easily and efficiently fixed.

A Simple Example

For good examples of formal specification at work I would suggest you try this Z case study or the case study for CASL in the CASL user manual. For those who want something more immediate I have a warning: To be short enough to present easily in this space the specifications are necessarily very simple and should be taken as a sample of the flavour of formal specifications rather than a serious example.

The specification for a simple stack, in SPARK, a version of Ada that adds formal specification semantics, would look something like the following:

package Stack
--# own State: Stack_Type;
--# initializes State;
is
        --# type Stack_Type is abstract

        --# function Not_Full(S: Stack_Type) return Boolean;
        --# function Not_Empty(S: Stack_Type) return Boolean;
        --# function Append(S: Stack_Type; X: Integer) return Stack_Type;

        procedure Push(X: in Integer);
        --# global in out State;
        --# derives State from State, X;
        --# pre Not_Full(State);
        --# post State = Append(State~, X);

        procedure Pop(X: out Integer);
        --# global in out State;
        --# derives State, X from State;
        --# pre Not_Empty(State)
        --# post State~ = Append(State, X);
end Stack;

The package body, containing the implementation, can then follow.

The own simply declares the variable State to be a package global variable, and initializes means that the variable State must be initialized internally in this package. We then declare an abstract type (to be defined in implementation) and some simple functions. The in and out keywords in the procedure declarations tag the parameters: in means that the parameters current value will be read in the procedure, and out means the parameter will be written to in the procedure. The global keyword declares the the package global variable State will be used in the procedure (and both read from and written to). The derives keyword provides explicit declarations of which input will be used in determining values for variables that will be output or written to. The pre- and post-conditions should be largely self explanatory.

As you can see, mostly all we are doing is making explicit exactly how we intend the procedures to operate. This specificity provides automated verification tools the information necessary to properly analyse and validate implemented code: Prior to a compile step you can run a verification and flow analysis tool that catches many subtle errors.

A similar object, specified in an algebraic specification language like CASL might look something like this:

spec Stack[sort Elem] =
        sort
                stack
        ops
                empty: stack
                push: stack * Elem -> stack
                pop: stack ->? stack
                top: stack ->? Elem
        axioms
                not def pop(empty)
                not def top(empty)
                forall s : stack; e : Elem
                          pop(push(s,e)) = s
                          top(push(s,e)) = e
end

CASL offers syntax that can compact this considerably, but this longer version makes the workings of the specification more clear.

We declare a specification for a stack of generic elements, of sort stack; and with operations empty (which is in a sense the constructor creating and empty stack); push which maps a stack and an element to a "new" stack; pop a partial function (denoted by the question mark) which maps a stack to "new" stack; and top another partial function which maps a stack to an element. We then define axioms: first, as pop and top are partial functions, we say they are not defined on empty stacks; secondly we declare that pop and top should behave as (partial) inverses for push for all stacks and elements.

This is sufficient information to completely specify stacks as a universal algebra and brings a great deal of powerful mathematical machinery to bear on the problem, much of which has been coded into a set of analysis tools for CASL.

While these examples are very simple, they should give you the flavour of how formal specification can work. Both SPARK and CASL support structured specifications, allowing you to build up libraries of specification, making them scalable to very large problems.

Why Use Formal Specification?

Why use static types? Why do any compile time checking? Why produce design documents for your software? Not every project is worth writing design documents for, and some projects are better off being developed quickly using a dynamically typed language and runtime checking. Not every project really needs formal specification, but there are a great many software projects that could benefit greatly from some level of formal specification - a great many more than make use of it at present.

I would suggest that it is probably unimportant whether your paint program, music player, word processor or desktop weather applet uses formal specification. What about your spreadsheet application? Bothering with formal specification for the GUI might be a waste of time. Bothering to do some specification for the various mathematical routines, ensuring their correctness, would potentially be worth the extra trouble. Formal specification doesn't need to be used for a whole project, only those parts of it that are sensitive to error. Likewise any network services could easily benefit from formal specification on the network facing portions of the code to significantly reduce the possibility of exploits: it is far easier to audit and verify code that has been properly specified. Security software, and implementations of cryptographic protocols, are far safer if formally specified: with cryptography the protocols are often rigorously checked, and many exploits relate to errors where the implementation fails to correctly follow the protocol. Finally mission critical business software, where downtime can costs millions of dollars, could most assuredly benefit form the extra assurances that formal specification and verification can provide.

None the less, barring a few industries, formal specification has seen little use in the past 25 years. Developers and software engineers offer many excuses and complaints as to why formal specification isn't suitable, isn't required, or is too hard. Many of these complaints are founded in a poor understanding of how formal specification works and how it can be used. Let's consider some of the common complaints:

But Formal Specification is Too Much Work...

Formal specification can be as much work as you choose to make it. You can do as little as adding contracts to critical functions or classes, or you can write the entire project from the top down by progressive refinement of (and verification against) a specification for which you have created formal proofs of all important properties. There is a sliding scale from a dynamically typed script with no documentation or comments, all the way up to a completely explicitly specified and proven system. You can choose the level of specificity and verification, and you can specify as much or as little of the system as you need. Formal specification covers everything from adding contracts to a couple of critical routines to complete specification of the entire project.

Formal specification isn't necessarily significantly more work than you do now. Writing contracts is only a little more work than static typing: you are simply declaring formally what you intend the function to do, something you ought to have a clear idea of before you write the function anyway. Writing a basic specification is only a little more work that writing a design document: you are simply formalising the diagrams and comments into explicit statements. For a little extra work in the initial stages you gain considerably in debugging and testing. Extended static checking based on contracts can catch many simple errors that would otherwise go unnoticed, and debugging is significantly accelerated by the added information contracts supply about runtime errors. If you've gone to the trouble of writing a formal specification, you can statically verify properties of the system before it is even implemented. Once implemented you can validate the implementation against the specification. When performing testing you can use the specification to help determine the best coverage with the least testing.

Formal specification does work in practice, and the gains in efficiency in testing and debugging can often outweigh the potential extra overhead during design. Design by Contract, for instance, is often cited as saving time in the development process, and there are many real world success stories where systems were developed faster by using contracts. A 20 person team completed in 5 months what took a team of 100 people using standard C++ almost a year. For projects where robustness is critical, full formal specification has been used successfully. Companies like Praxis High Integrity Systems use formal methods successfully in the rail, aerospace, nuclear, finance and telecommunications industries (among others), and have sold their formal method tool-set to a variety of large companies. Reading through some of their recent work and case studies makes it clear that formal specification and verification can prove to be more efficient and faster to use.

But Formal Specification is Not Practical...

On the contrary, formal specification is used all the time in many industries, and there are various companies like Praxis High Integrity Systems, B-Core, Eiffel Software, Kind Software, and Escher Technologies who provide formal specification tools as a major part of their business.

Formal specification has proved to be practical in the real world. What it has lacked is mature tools to make development using formal specification faster and easier (try writing code without a good compiler; try doing formal specification without good static checking tools), developer awareness, and developers skilled in the languages and techniques of formal specification. It doesn't take much to learn - learning a specification language is not much harder than learning a programming language. Just as programming appears to be a difficult and daunting task to a person who doesn't know any programming languages, specification looks difficult and impractical to people who don't know specification languages. Take the time to learn and your perspective will change.

But the Project Requirements are Always Being Changed...

It is true that many projects face ever changing requirements. The question is not whether this renders formal specification useless (it doesn't) but how formal specification compares to informally specified software in such a situation.

First of all it should be noted that engaging in formal specification can help reduce the problem to begin with. By requiring you to rigorously specify at least some portions of the software, formal specification can assist in finding ambiguities, cases that were not covered, and other problems much earlier in the development cycle when changes are easiest to make. Those parts of the system, such as GUIs, that are often the target of more whimsical design or requirements changes are precisely the parts that benefit least from, and are least likely to use, formal specification. Changes to design or requirements for those parts of the system, then, are not likely to be more detrimental than for informally specified projects.

Secondly formal specification is quite capable of dealing with change, and even offers benefits in the face of changing requirements. A change in requirements results in a change in specification, but because the specification is formally written the impact of the changes can be analysed. You can check that new requirements remain consistent with the rest of the system. You can also determine all parts of the system that will be impacted by the change and avoid bugs introduced by the changes. Having a formal specification for the system when a change in requirements occurs makes it easier to see how the change will effect the system and easier to make the changes consistently and completely. Formal specification can make changes in requirements easier to deal with, not harder.

But I Already do Unit Testing...

Unit testing is fantastic, and there's no reason to stop just because you can write proofs for some aspects of your code. Unit testing is not a replacement for formal specification however. Testing only verifies the component for a very limited and specific range of cases. Specifically testing covers the cases that the developer thought of. A great many bugs, however, are those that occur from situations the developer didn't consider, and probably wouldn't have included in his test. You can improve the situation with testing tools like fuzzers, but you're still only checking a sampling of the whole space. Formal specification, on the other hand, allows construction of formal proofs that cover all possible cases. I would much rather specify and prove Pythagoras' theorem than simply assume it is true by testing it on random right angled triangles. Likewise, while testing is valuable (and easy) when assurance matters it is no replacement for proof based on a specification.

Does this mean you should give up Unit testing? In no way shape or form. Just as formal proofs in mathematics are much harder than trying a few cases, formal proofs from specifications require significant work - you most likely can't prove everything. That means the best method is prove those properties that are critical, and continue testing the system much as you normally would. Hopefully you'll see a lot less errors to debug based on the extended static checking of course.

But Formal Specification Still Can't Guarantee Perfect Software...

Correct, there are no guarantees. Complete proofs are often too complicated to perform, so theorem proving for specific properties is usually undertaken instead. Static checking can be enhanced significantly with suitable specifications, but not all errors can be caught. Your software is only going to be as stable and secure as the system it is running on. If you can't be perfect why try at all? Because significant gains can be made and the costs may be smaller than you think. Even if the whole system can't be proved, managing to prove key properties may well be all the assurance of correctness that is required for the application at hand. Even if you can't catch all the errors statically, reducing the number and severity of runtime errors can bring significant efficiency gains in the testing phase. Furthermore the cost of errors in software found after release can be sufficiently high that any reduction is worthwhile. Finally if you can't trust your compiler and operating system, then everything is compromised. At some level you have to trust something - we all trust a great deal of software right now that we expect to have flaws - reducing the source of errors to trusted components is still a significant gain.

But Formal Specification Is Only Viable for Trivial Examples...

Not even close to the truth. Formal specification and formal methods have been used for large projects involving hundreds of thousands of lines of code. Just look at many of the examples provided above: these were not small projects, and they were not toy trivial examples; these were large scale real world software systems. Examples of formal specification tend to be small simplistic cases because they are meant to be just that: easily comprehensible examples. In the same way that programming languages often use "Hello World" and quicksort as examples, formal specification languages use equally simple but demonstrative examples. Don't take this to mean that the language and method doesn't scale.

Conclusions

Formal specification isn't a silver bullet, and it isn't the right choice for every project. On the other hand you can use as much specification and verification as is suitable for your project. You can apply formal specification only to the portions that are critical, and develop the rest normally. More importantly, the techniques, languages and tools for formal specification continue to improve. The more powerful the methods and the tools, the more projects for which formal specification becomes a viable option. In an increasingly network oriented computing world where security and software assurance is becoming increasingly important, the place for formal specification is growing. If you are a software engineer it makes sense to be aware of options available to you.

Apple make shiny toys, there is no denying this. It is a shame that their customer support and build quality are so dire. About a year ago, I decided I should send my PowerBook in for repairs. It was not an easy decision, there were a few things wrong with it (white spots on the screen, one of the SO-DIMM slots not working, detection of headphones had an intermittent fault), but nothing that made it unusable - and I used it a lot. Never mind, I thought, it usually only takes them two days to do a repair, so I'll back everything up, grit my teeth, and send it in.

A month later they finally admitted that they'd lost it. A month after that they got around to replacing it. The one they replaced it with didn't even boot. They collected it and fixed it relatively quickly, leaving me with a new machine which had a fault in one of the SO-DIMM slots.

At this point, I decided not to send it back in for repair again. I'd already wasted around 10 hours on hold to Apple's customer support, and I didn't want to spend any longer.

Now, however, the fault with one slot has become an intermittent fault with both. Moving the machine at all causes memory errors (and will cause it not to resume from standby). When I boot, I have no idea which RAM slot will be operational (I've put a stick in each - sometimes I boot with 512MB, sometimes with 256MB. So far, I haven't managed to boot with 768MB, but there's hope...).

I am going to try to borrow a machine from the department while I wait for this one to be repaired. If I am really lucky, I'll be able to bring it home and work from here. Well, I can hope...

This week I got some new toys. I think my supervisor is feeling guilty (been seeing other students, or something), and practically forced me to spend some grant money on shiny things. These were:

• An Apple 23" Cinema HD. Very nice. I'm using it now. I have so much screen space that I can actually see my desktop in several places (unlike my physical desktop, which is covered with things).
• A LaCie 500GB disk (which is really 466GB). FireWire 800, with FW400 and USB2 as well (although you can only chain them with FW800). I have a 320GB (300GB) one at home, which I use for video editing. This one is for storing large data sets, and definitely not for video editing, oh no. Honest.
• An iSight. Officially so I can join video conferencing meetings with the other 3 sites we work with on my laptop.
• A BlueTooth Keyboard (Apple) and mouse (Kensington - 3 buttons!) so I don't need to plug in lots of wires when I plug in my laptop.

I suddenly have an incentive to stay at my desk (apart from the view of the sea).

In unrelated news, I mentioned previously that I was putting OpenBSD on a co-located Mac Mini, and would be writing about this. The first 4 of these are now online:

Macs in a rack - taking the mini to the masses
Why OpenBSD?
Setting up secure mail on OpenBSD
Filtering Spam with OpenBSD

The fifth one (Web and Webmail) is done, but will not be release until next Friday (it's my birthday next week, so I wrote it early). The sixth will cover setting up a Jabber server. I haven't yet decided what the seventh will cover - suggestions welcome...

Oh, and the hosting place has agreed to give a discount to Ping Wales readers, so don't forget to mention Ping to them if you do decide to use them (details in the first article).

I finally decided to order a Mac Mini. Not as a desktop, but as a colocated server (with the company featured on Slashdot a while back). One thing that they don't advertise is that their `remote hands' service allows you to change operating systems. While I am very pleased with OS X as a desktop, I would rather have something a little more command line oriented on a server (yes, I know you can do most things on the command line with OS X, but it is not really designed for it). To this end, I shall be installing OpenBSD on it as soon as it arrives. This means that I will have a 1.42GHz RISC system running OpenBSD with 20GB of bandwidth a month for $22.99. The closes competitors I found for this were several times the price for a similar service - largely due to the fact that they required 1U systems which cost a whole lot more to host.

Once the system is set up and running, I will post more details.

On my /. front page, I have the two sections I most frequently read in little boxed, BSD and Apple. The Apple box is completely full of April Fools' `Jokes', while the BSD box is completely full of real stories. The seems slightly bizarre, since there are so many opportunities to generate convincing April Fools' stories for *BSD (I seem to recall one last year claiming that FreeBSD was going to start using the Linux kernel), and yet no one bothered. I'll have to remember to write one next year.

Might as well use this journal for rants, I suppose...

I've finally managed get myself set up with ADSL on Linux. I went with Demon, as they've got a decent reputation, and their web page states:

"Host software support for:

• Windows 98, 98SE, 2000, ME and XP
• Mac OS 8.6,9 and X
• Linux

Great! However, after the package arrived, I couldn't help noticing a few obvious differences between the "host software support" for Windows vs Linux:

• The CD contains Windows drivers for the USB modem. There are no Linux drivers (and you have to mount it with rock-ridge extensions disabled to see anything at all, which wasn't obvious).
• There are detailed step-by-step instructions showing how to set it up on Windows. Linux isn't mentioned on the printed copy, and the CD version contains a single line, telling you to download drivers from the 'net (How? I don't have drivers for my modem!! Didn't anyone spot this little problem when they wrote the instructions?)
• When I phoned up for support and said I was installing on Linux, the response was "Ha! Good luck!". Not what you want to hear. I pointed out that Linux is one of their supported systems but apparently "We don't have any training for that."

The problem was that the CHAP authentication was failing (I'd downloaded some drivers from sourceforge via my mobile phone's irDA port - painfully slow, but it worked). The helpdesk chap was friendly, but didn't seem able to suggest anything.

I got fed up and bought myself an ADSL modem router. Exactly the same problem. But this time when I phoned up and said I had a router, they suddenly had a whole load of useful test addresses to try which quickly narrowed the problem down to BT's exchange. Grr. BT fixed it after a couple of days, and it's all been fine since, but I think describing Linux as supported is really stretching things!

Slashdot is full of political trolls. These are people who advocate political ideas dishonestly and disrespectfully, and abuse and insult users who question or threaten their (often dubious) worldview. We cannot help the deficiencies in America's educational system, nor can we force people to have morals or civility, nor can we stop them from abusing the moderation system, and (this being America) we would fight to the death to defend their right to speak their mind (no matter how depraved their impulses), but, and this is the important thing, we are not obligated to listen to them, either.

PoliticalTrollOptOut is a service. Simply, we identify political trolls and add them to our Foes list. This allows others to use our work for study, or, more importantly, to enhance their slashdot experience.

Anyone who wants can make us their Friend will see all the trolls we identify as Foes of Friends. This "warning signal" can save you a lot of trouble. And if that's not enough, you can use your slashdot preferences to hide (or make prominent, and study) posts by the Political Trolls we identify, by adjusting the score modifier for "Foes of Friends." It's that simple.

Do you hate getting sucked into pointless arguments by people who actually derive satisfaction and enjoyment from your outrage? Tired of arguing with people who are knowingly and smugly being dishonest? Need a break from the growing wave of nutty reactionary posting and moderation?

If slashdot's moderation system isn't cutting it for you, we can help. Just crank their scores down and watch them disappear. Just imagine, if we all did it, they would be left talking to themselves.

Are you a moderator today? Switch it the other way, and use PoliticalTrollOptOut as a quick reference for known troublemakers.

One thing we don't encourage is moderating with trolls filtered out. Where's the fun in that, anyway?

So I just make you my friend? It's that simple?

Sure! If you like, though, we encourage everyone using our service to spread the word by linking to this journal in their signature, with something like this:

Tired of Political Trolls?
<A HREF="http://slashdot.org/~PoliticalTrollOptOut/journal">Opt Out!</A>

We know what you're thinking: what constitutes a political troll? How can we make that call? And, how can any one person or group possibly catch them all?

Let's be realistic. What crosses this line is not something everyone is going to agree on. Furthermore, as is the style these days, everyone actually will disagree on it. Anyone we flag will assume we're their political opposition. Conservatives will call us liberals, and vice versa. We know who we are dealing with; we are going directly after slashdot's worst of the worst. They will not politely disagree with us. They will say we are biased, crazy, hypocritical, that we flag anyone we dislike, that we even eat babies. They'll claim every person we haven't flagged yet is proof of our failure, bias, or evil. They will call us censors and Nazis and child molesters and every other evil thing they can think of. Some of them will put more energy and creativity into derailing and destroying us than they put into their homework, spouses, or jobs.

If the trolls weren't really this bad, we wouldn't need to bother with this in the first place.

All you are really doing is deciding to pick us as an editor. You can look at every decision we've made so far, look at our Foes list and read what is written here, and decide for yourself based on the evidence whether you think we're useful, and if you trust us to keep it up.

We make these decisions based on some basic tests. We do our best to be fair and non-partisan, and apply our standards without any regard for whatever position anyone is actually advocating. Of course you could have a "ConservativeOptOut" or a "LiberalOptOut" - in fact, I encourage it! But that's not us. We flag them all, whatever stripe they claim to be. They're really not that different anyway.

What are those tests?

1. There are many trolls; is this one clearly a political advocate, crank or ideologue?
2. Are they being abnormally personal, rude, condescending, disrespectful, or mean? Do they engage in stalking (following "enemies" into other threads to harrass them) or threats?
3. Are they propagating widely known and discredited misinformation or propaganda (i.e. "Who was behind 9/11 again?"). Note that we tend to apply this one only when it's really blatant, not for things that could conceivably be legitimately disputed.
4. Are they being clearly disengenuous, arguing in bad faith, using debater's tricks, misquoting or lying about foregoing posts? Are they engaging in slander/libel? Making big claims and refusing to cite sources?
5. Are they conspicuously imitating, plagiarizing, or attempting to use as authoritative citations, known political propaganda organizations, bent think tanks, "*-wing" blogs, or other discredited or disreputable party mouthpieces?
6. We consider this project to be reasonable and fair. People we flag will disagree and will naturally troll us too, in a variety of ways, for instance, falsely reporting others as political trolls. We will not refuse to flag people just because the object of their political trolling is us.

This is it. We're not attorneys; if you want a more precise definition for what we do and how we do it, look at our track record.

Obviously, we can never catch them all. Even if we could, anyone can stop posting from one account and make another. There is a little penalty for that - no karma, no karma bonuses, and inconvenience - but it's not enough to stop them. Slashdot generates more text in a day than most people can read in a week, and this is a volunteer effort.

That means that any troll can (and will) point to another troll that hasn't been flagged yet and cry "unfair," "biased," etc etc. They're hoping you'll be fooled, but I'm sure you're smarter than that.

None of these problems are so serious we shouldn't try, and try we shall. We will never flag them all, but if we can get quite a few. Over time we will continue to improve, and fairly quickly what we offer will become substantial enough to be useful.

What? How are we supposed to talk about politics without being labeled a political troll?

That's easy. We've been doing this for many millenia, and it's the source of almost all of our progress as a species. Nerds: try to think about a political idea like a software engineering idea. You may believe in it, you may even have thought of it yourself and be really attached to it, but you can't really swear it's perfect and bug free, can you? In other words:

1. Be absolutely, scrupulously honest
2. Be respectful, tolerant, and keep your sense of humor
3. Be forthright; clearly say what you mean
4. Be prepared to be wrong
5. Be prepared to be right but part as friends with someone you haven't convinced of it
6. Don't make judgements, ask questions (This works so well you will end up swearing by it!)
7. Don't imagine your ideas or beliefs are obvious to anyone
8. Pretend you are a scholar. If you already are a scholar, pretend you are a great scholar. Never say something is a fact unless you can back up with references.
9. When citing sources, use reputable ones. The more reputable, the better your argument looks. Something isn't automatically a lie because it comes from a particular place; simultaneously, it's silly to use a shady, discredited, or obviously biased source. Citing the Enquirer doesn't make your Batboy argument stronger, neither can Bill O'Reilly or Dan Rather help your case much about the Bush family or the "vast left-wing conspiracy."
10. If you get something wrong, apologize and admit it. (You have no idea how classy this looks, or how stupid you look lamely trying to cover up a mistake)
11. Refrain from immediately assuming an error on someone's part is malicious. If it's an accident, you'll never help them without respecting them, and if it's not an accident, it'll become pretty clear soon enough. Don't jump on it, just keep asking questions.
12. When conversing with a stranger, pretend you are talking to your grandmother. Unless you hate your grandmother. Then, just pretend you are talking to your best friend who may really agree with you, but is playing devil's advocate
13. You will be mocked, insulted, slanedered, misinterpreted, and otherwise abused in every conceivable way. That's life. Keep speeking the truth; if you've got that covered there really no need to get that nasty in return. (You have no idea how much better you'll look than the other guy)

When you talk politics with somebody, you and they are on the same team. Your goal in this game is to both learn and advance your knowledge by pooling your resources, finding the weak points in your ideas, adapting, and growing.

You're like good attorneys practicing old-fashioned adversarial justice. You may want your side to win, but you are not trying to win at all costs. You all want the truth to win in the end, or you both lose. I know it sounds crazy, but it's true!

I found a troll! Quick, flag them!

For the time being, we maintain a separate user that usually has an open journal. It's here. You can use it for the reporting of new candidates. We used to have a journal on this user, below, but they expire, and then making new ones messes up the order, etc etc.

We make no guarantees. The journal may be open or it may not. We may read it, or we may not. We may follow it, or we may not. We generally do not reply to suggestions.

So far, the suggestion box has been most useful for trolls to report themselves by trolling there without being anonymous. Almost the entire contents of the reports are typically trolls doing predictable things: pissing, moaning, false reports, accusing us of various nefarious acts of bias and conspiracy, posting gay porn, etc.

If your post doesn't include a detailed description, with links to the best examples you can find of their behavior, we ignore it.

If you say "so and so is lying, trolling, etc." without providing links to back it up, we ignore it.

You only have so many foes slots.

That's right. As we run out of slots, we'll create more users. We'll post a notification if/when that happens.

It's impossible to be unbiased!

Not at all.

It's impossible to be "perfectly fair." But you can do a good job and get close enough for everyone's needs.

Anyone who claims they are unbiased, is not trustworthy.

Technically, it's anyone who makes illogical arguments who is untrustworthy.

Some people are fair and unbiased. Others aren't, but claim they are.

The only way to tell them apart is to evaluate their claims with observable facts.

Luckily, if you are evaluating PTOO, all the facts are right here, at your fingertips. Follow some links and make your own conclusions.

You have more people from one party than another in your list. This is proof that you're biased.

I imagine we'd have to maintain exactly the same number of party X versus party Y trolls to make this one go away.

Why just political trolls?

People act like asses for a lot of reasons, that's true. Maybe a plain old "TrollOptOut" would be useful. If you think so, go for it, don't let me stop you. I track the political ones because I find them particularly insufferable. Maybe it's the egomaniac, control-freak mentality that draws people into politics. Maybe it's just that there are more of them. One big thing about them is that they tend to resist the moderation system the best. Since they rally around a cause, a like-minded group of them will often end up with mod points, and they never use them impartially. The best of them sometimes make surprisingly sophisticated (and labor-intensive) attempts to game the moderation system.

By contrast, I kind of respect the straight-up hardcore anarchist trolls. Those guys don't give a crap about karma or winning friends and influencing people. They have no agenda at all, except to piss off or freak out as many people as possible. Many would disdain and even avoid stooping to politics to twist somebody's tit. Sometimes I find them kind of funny, actually.

Most of what this user posts is not trolling!

Of course not.

There are a few rare ones who do nothing but troll. Most are normal, friendly even interesting people who can make highly informative posts about Sendmail configurations or Thai venereal diseases. It's just that once every 100 posts the editors release a political story, and the full moon comes out, and then you better look away, it's ugly.

There are literally hundreds of thousands of people who participate here. I am perfectly happy to lose the ones who have engaged in political trolling, even if they don't do it "that often." There is plenty left over.

A troll has sucked a bunch of people into an argument. One of the responders get nasty. Are they both "Political Trolls"?

Not really.

I like to start with the low-hanging fruit: the people who instigate the fight. The ones who go over the top. There are plenty of these without going depth-first into all the debatable cases. I do usually watch the ones I'm not sure about for a while to see if they have a pattern.

What can I do if I disagree with a decision?

Someday there will be software that lets us get into a giant automated election about every decision we make. For now, decisions are made by me, and in the future, anyone I choose to share this account with. You can assume any such person will make roughly similar judgements as I would.

I've been flagged as a troll! Not fair! Waaaaah!

Yes, we are aware that you disagree with everything we've said about you, and that none of you believe you have been judged fairly.

Duh. This is rule number one in the political troll's playbook.

You have not been censored. We, and our friends, may choose not to listen to you, and you have no right to force us to.

You got flagged because you were caught engaging in political trolling. You have your opinion about what you said, and we have ours. Goodbye.

Surely you must admit you are not infallible. Is there any process for appeal?

The problem is abuse. There are not many ways to do this that are scalable and sustainable against the kind of abuse generated by a large group of professional abusers.

Thus, the short answer is, no. We rely on our judgement, and we give you the opportunity to as well. That's all we can offer.

• damiangerous
• daveschroeder
• AtariAmarok, aka Concern Is A Faggot, sammeal
• N8F8
• ccmay
• SamBeckett
• Jim_Callahan Jim_Callahan
• Kohath
• HanzoSpam
• Jerf Jerf
• Juggle
• danheskett
• Megaweapon Megaweapon
• That's Unpossible!...(reply)...That's Unpossible!
• sadomikeyism
• randallpowell
• Anita Coney
• PortHaven PortHaven
• ifwm ifwm
• Master of Transhuman
• magarity magarity

Yesterday, Slashdot linked to something I wrote for the first time. Depressingly, this is possibly the least coherent rambling I have ever written (I'd drunk a lot of caffeine and was in a hurry) - even including most of my comments on Slashdot. Ho hum.