April 10, 2012

Simulator performance -- Ymer 3.0.5 vs. 3.0.6

When I first developed Ymer, I was concerned about probabilities of outcomes not summing to one if I represented them as floating-point numbers. I therefore wrote a Rational class to have an exact representation of probabilities. The class was used throughout the code to represent any number. To avoid overflow issues as much as possible, I made sure all rational numbers were stored in reduced form, which meant frequent computations of greatest common divisor.

In reality, the loss-free precision was an illusion, since the model-checking algorithms in Ymer were implemented using floating-point arithmetic. I recently replaced the inefficient Rational class with a more lightweight TypedValue class for representing numbers:

class TypedValue {
 public:
  enum Type { INT, DOUBLE, BOOL };

  TypedValue(int i) : type_(INT) { value_.i = i; }
  TypedValue(double d) : type_(DOUBLE) { value_.d = d; }
  TypedValue(bool b) : type_(BOOL) { value_.b = b; }

  Type type() const { return type_; }

  template <typename T> T value() const;

 private:
  Type type_;
  union {
    int i;
    double d;
    bool b;
  } value_;
};

template <typename T>
T TypedValue::value() const {
  switch (type_) {
    case INT:
      return value_.i;
    case DOUBLE:
      return value_.d;
    case BOOL:
      return value_.b;
  }
}

This class still has some overhead for arithmetic operations. It is really just meant as a representation of numbers in a parsed model, which would then be compiled into a more efficient representation for the simulator to use. Nevertheless, just replacing Rational with TypedValue has resulted in a measurable performance improvement. This change was introduced in Ymer 3.0.6. The graphs below compare simulator performance between Ymer 3.0.5 and 3.0.6 on two benchmarks from the PRISM benchmark suite. Each data point represents the time to generate 10,000 sample paths of length 1,000.

No comments:

Post a Comment