Ymer 3.0.9

More refactoring, focused on improving the representation of variable assignments in states, has resulted in further performance improvements. This new version of Ymer is up to 36% faster than the previous version on select benchmarks.

Ymer 3.0.8

Cleaning up and refactoring the code for Ymer helped me discover a memory corruption bug in the parser, which is fixed in this version. The bug was especially apparent when using the ‑‑const command-line flag for setting the value of uninitialized model constants, and could result in bad models. I also fixed a test that was failing to compile with GCC 4.2.

The perils of implicit conversions in C++

In my last post, I was boasting about improved simulator performance in Ymer. Unfortunately, the results for the tandem queuing network were invalid due to a bug introduced in Ymer 3.0.6. I fixed the bug and quickly released version 3.0.7. As seen below, there is still a boost from getting rid of the Rational class in Ymer—just not quite as big of a boost as I first had thought.

The bug was due to implicit conversion from const char* to bool. The Rational class had a single-argument constructor that parsed a C string into a rational value. The replacement TypedValue class did not have a corresponding constructor, but it did have a constructor for implicitly converting values of type bool to TypedValue. As it turns out, C++ permits implicit conversions from any pointer type to bool, so inadvertently there still was a way to implicitly convert a C string to a TypedValue. This implicit conversion was happening in the code that parsed constant overrides (needed for the tandem queuing network model), which resulted in all parsed constants to have value 1 (non-null pointer converted to bool). It explains the artificially flat performance across tandem queuing network model sizes for Ymer 3.0.6, and in hindsight I should have been more suspicious about it.

To prevent future occurrences of the same bug, I have added a private constructor to the TypedValue class that matches any pointer type. When the compiler encounters an attempt to implicitly convert a pointer type to TypedValue, an error is emitted because the matching constructor is private. For further protection, the constructor does not have an implementation, so we would still get a link error if we invoke the constructor in a context where it is accessible.

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:
  template <typename T>
  TypedValue(T*);

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

This bug, of course, demonstrates the importance of tests. There should have been a test that exposed the bug before it got released. I had actually added a unit test for the TypedValue class using the Google C++ testing framework, but needless to say it did not cover the erroneous conversion from a C string to TypedValue that happened in the parsing of constant overrides provided as a command-line argument.

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.

Ymer 3.0.6

Version 3.0.6 of Ymer was released today, with some small performance improvements to the simulator. The new version is 10-30% faster on select benchmarks.

As of version 3.0.5, Ymer compiles on Mac OS X 10.6 Snow Leopard with XCode.

Starting with this version, I am shifting my effort from a complete rewrite to targeted refactoring of the 3.0 code base for Ymer. I have learned a lot from trying to rewrite Ymer from scratch, but I think I will make faster progress by incorporating my ideas for improvements into the existing code. Version 3.0.6 is the first of what I hope will be a series of releases with measurable performance gains.

Ymer 3.0.4

Version 3.0.4 of Ymer, released yesterday, contains a couple of features that help with performance evaluation of the tool itself:

• Support for fixed sample sizes and path lengths, making it easier to evaluate the performance of the simulator implementation alone.
• Support for TCMalloc, enabling CPU and heap profiling using gperftools.

Ymer is hosted on Google Code.

Ymer 3.0.3

Version 3.0.3 of Ymer, released today, contains minor improvements to the parser. The improvements allow Ymer to parse more PRISM models without requiring modifications, which should make it easier to run benchmark tests.

The following improvements were made:

• Support for uninitialized constants and constant initialization from command line. For example, if a model has an uninitialized constants N and M, then you can set the value of N and M from the command line with ‑‑const=N=2,M=3.
• Support for true and false in guard expressions.
• Support for addition and subtraction in rate expressions.
• Parser support for rewards specifications to avoid parse errors for model files that contain rewards specifications, but rewards specifications are otherwise ignored.

Ymer is hosted on Google Code.