In this note, we will introduce a concept of modularity of exact categories due
to Masana Harada. The naming is coming from the classical modular lattices
theory. We will also state and prove so-called homotopy
Grayson-Staffeldt-Jordan-Holder theorem which is implicitly appeared in [Gra87]
and [Sta89]. The theorem says contractibility of a simplicial set associated to
a certain upper semi-lattice. Combining these two ideas and utilizing
Waldhausen's technique in [Wal85], we will get a devissage theorem for modular
exact categories with weak equivalences which is a generalization of original
Quillen's one in [Qui73].
[January 28 version replaced February 1. An "idempotent completeness
assumption" has been removed.]