Erreichbarkeitsprobleme für parallele Programme mit Locks sind oft nahe an der Grenze zur Unentscheidbarkeit. Wir zeigen ein neues, flexibles und praktisches Programmmodell durch Betrachtung einer Erweiterung von Dynamischen Pushdown-Netzwerken (DPN). DPN sind ein Modell für parallele Programme mit Rekursion und dynamischer Threaderzeugung, das früher schon Erreichbarkeitsanalysen unterzogen wurde. Wir erweitern DPNs um dynamische Lockerzeugung und zeigen, dass locksensitive Erreichbarkeit bei Verwendung von nicht-reentrantem Locking für dieses Modell entscheidbar ist. Wir nutzen die Entscheidbarkeit der Erfüllbarkeit monadischer Prädikatenlogik zweiter Stufe (MSO) auf einer von einer Hyperedge Replacement Grammar (HRG) erzeugten Graphenmenge. Dazu reichern wir die in unserem Modell vorkommenden Ausführungsbäume mit geeigneten Elementen an, geben eine HRG zu diesen Graphen an, und verwenden MSO, um die Eigenschaften von Graphen auszudrücken, die locksensitive Erreichbarkeit bezeugen.