Formalizing, Analyzing, and Extending the Model of Bulk SynchronousParallel Computers